The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.

Extracting ω's programs from proofs in the calculus of constructions

The work

AuthorsChristine Paulin-Mohring
Editors
Typemisc
Year1989
Citekeypaulinmohring1989extracting

Where it appeared

Published inACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
Pages89--104

Identifiers

DOI10.1145/75277.75285
OpenAlexW2086054252

Access

Landing pagehttps://doi.org/10.1145/75277.75285

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

Abstract

We define in this paper a notion of realizability for the Calculus of Constructions. The extracted programs are terms of the Calculus that do not contain dependent types. We introduce a distinction between informative and non-informative propositions. This distinction allows the removal of the “logical” part in the development of a program. We show also how to use our notion of realizability in order to interpret various axioms like the axiom of choice or the induction on integers. A practical example of development of program is given in the appendix.

How it got here

How it got hereagent via openalex
Added2026-10-24 12:36 UTC
Not denied bya person 2026-10-29 17:12 UTC

Cite it as

@misc{paulinmohring1989extracting,
  title        = {Extracting ω's programs from proofs in the calculus of constructions},
  author       = {Christine Paulin-Mohring},
  year         = {1989},
  journal      = {ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)},
  pages        = {89--104},
  doi          = {10.1145/75277.75285},
}

This record lives at https://refs.drheap.org/paulinmohring1989extracting/ and will keep doing so.