Extracting &ohgr;'s programs from proofs in the calculus of constructions

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.

REFERENCES

• 1: M.J. Beeson. Foundations of Constructive Mathematics, Methamathematical Studies. Springer- Verlag, 1985.
• 2: C. BShm and A. Berarducci. Automatic synthesis of typed )~-programs on term algebras. Theoretieal Computer Science, 39, 1985.
• 3: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• 4: Th. Coquand. Metamathematical investigations of a calculus of constructions, part I: syntax. 1987. To appear as INRIA Technical Report.
• 5: Th. Coquand. Une Thdorie des Constructions. Th~se de 3~me cycle, Universitd Paris 7, 1985.
• 6: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 7: Th. Coquand and G. Huet. Concepts mathdmatiques et informatiques formalis~s dans le calcul des constructions. In The Paris Logic Group, editor, Logic Colloquium '85, North-Holland, 1987.
• 8: Thierry Coquand , Gérard P. Huet, Constructions: A Higher Order Proof System for Mechanizing Mathematics, Invited Lectures from the European Conference on Computer Algebra-Volume I, p.151-184, April 01-03, 1985
• 9: P. Dybjer. Program Verification in a Logical Theory of Constructions. Technical Report, Programming Methodology Group, Chalmers University of Technology and University of GSteborg, 1986.
• 10: S. Hayashi and H. Nakano. PX, a Computational Logic. Technical Report, Research Institute for Mathematical Sciences, Kyoto University, 1987.
• 11: W.A. Howard. The formulae-a.s-types notion of constructions. In J.P. Seldin and J.R. Hindley, editors, to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism., Academic Press, 1980. Unpublished 1969 Manuscript.
• 12: J.-L. Krivine and M. Parigot. Programming with proofs. 1987. Preprint, presented at 6th symposium on Computation Theory, Wendish- Rietz, Germany.
• 13: C. Mohring. Algorithm development in the calculus of constructions. In Symposium on Logic in Computer Science, IEEE Computer Society Press, Cambridge, MA, 1986.
• 14: B. NordstriSm and K. Petersson. Types and specifications. In R.J~.A. Mason, editor, Information Processing 88, North-Holland, 1983.
• 15: P. Martin-LSf. Intn',iiionislic Type Theory. Studies in Proof Theory, Bibliopolis, 1984.
• 16: Michel Parigot, Programming with Proofs: A Second Order Type Theory, Proceedings of the 2nd European Symposium on Programming, p.145-159, March 21-24, 1988
• 17: A.S. Troelstra, editor. Melamalhemalical {nvesligalion of In~uition.istic Arithmetic and Analysis. ~,NM S44, Springer-Verlag, 1973.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Languages, Theory, Verification