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

Authors: 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}
  }