## Paper: Algorithm Development in the Calculus of Constructions (at LICS 1986)

**Christine Mohring**

### Abstract

We present the development and proof of algorithms, written in
the Calculus of Constructions of Th. Coquand and G. Huet. Programs are
realized as typed λ-terms from where we can extract a pure λ-term
which represents the computable part of the algorithm. Type verification and
therefore correctness of programs is mechanically checked by the system, a
prototype implementation of the Calculus in the language ML.

The study of these examples shows that it is possible to code programs, jointly
with their proofs, in the Calculus of Constructions. We will briefly present
this calculus and then describe examples, using part of them in order to
illustrate the main remarks which issue from this work.

### BibTeX

@InProceedings{Mohring-AlgorithmDevelopmen, author = {Christine Mohring}, title = {Algorithm Development in the Calculus of Constructions}, booktitle = {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)}, year = {1986}, month = {June}, pages = {84--91}, location = {Cambridge, MA, USA}, publisher = {IEEE Computer Society Press} }