×

Verifying programs in the calculus of inductive constructions. (English) Zbl 0905.68092


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

LEGO; Nuprl; Coq; Automath
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barendregt, H.:Lambda Calculi with Types. Handbook of Logic in Computer Science, Volume 2, 1991.
[2] Burstall, R. and McKinna, J.:Deliverables: a categorical approach to program development in type theory. Technical Report 92-242,LFCS, October 1992. Also in [NPP92].
[3] Cornes, C., Courant, J., Filliâtre, J. C, Huet, G., Manoury, P., Paulin-Mohring, et al.: Coq V5.10 Reference Manual. INRIA technical report 0177, July 1995.
[4] Constable, R. L., et al.:Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.
[5] Coquand, T.:Une théorie des constructions. PhD thesis, Université Paris VII, 1985.
[6] Coquand, T.: Meta-mathematical investigations of a Calculus of Constructions, in [Hue89], 1989.
[7] de Bruijn, N. G.: A survey of the project AUTOMATH. In Hindley, J. R., editor,To H. B. Curry: Essays on Combinatory Logic, lambda-calculus and formalism. Seidin, J.P., 1980.
[8] Girard, J. Y.:Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris 7, 1972.
[9] Hoare, C. A. R.: An Axiomatic Basis for Computer Programming.Communications of the ACM, 12(10), October 1969. · Zbl 0179.23105
[10] Howard, W. A.: The formulae-as-types notion of construction. In Hindley, J. R., editor,To H. B. Curry: Essays on Combinatory Logic, lambda-calculus and formalism. Seldin, J.P., 1980.
[11] Howe, D.: Reasoning About Functional Programs in Nuprl. InFunctional Programming,Concurrency, Simulation and Automated Reasoning, volume 693 ofLNCS, 1993.
[12] Huet, G.: The Calculus of Constructions, Documentation and users guide, Version 4.10. Technical report, INRIA, 1989.
[13] Luo, Z. and Pollack, R.: LEGO Proof Development System: User’s Manual. Technical Report 92-211, LFCS, May 1992.
[14] Luo, Z.:An Extended Calculus of Constructions. PhD thesis, Department of Computer Science, University of Edinburgh, June 1990.
[15] Martin-Löf, P.:Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, 1984. · Zbl 0571.03030
[16] [MaS92] Manoury, P. and Simonot, M.:Des preuves de totalité de fonctions comme synthèse de programmes. PhD thesis, Université PARIS 7, December 1992.
[17] Nordström, B., Petersson, K. and Plotkin, G., editors:Proceedings of the 1992 workshop on types for proofs and programs, June 1992.
[18] Nordström, B., Petersson, K. and Smith, J. M.:Programming in Martin-Löf’s Type Theory: an introduction. Oxford Science Publications, 1990. · Zbl 0744.03029
[19] Parent, C.: Developing certified programs in the system Coq ? The Program tactic. In Barendregt, H. and Nipkow, T., editors,Types For Proofs and Programs, volume 806 ofLNCS, pages 291-312, May 1993.
[20] Parent, C.:Synthèse de preuves de programmes dans le Calcul des Constructions Inductives. PhD thesis, Ecole Normale Supérieure de Lyon, January 1995.
[21] Parent, C.: Synthesizing proofs from programs in the Calculus of Inductive Constructions. InMathematics for Programs Constructions ’95, volume 947 ofLNCS, 1995.
[22] Parent-Vigouroux, C.: A proof example of a division algorithm with the Program tactic in Coq.Formal Aspects of Computing 9(E), (1997). http://www.cs.man.ac.uk/ fmethods/facj · Zbl 0905.68092
[23] Pfenning, F. and Paulin-Mohring, C.: Inductively Defined Types in the Calculus of Constructions. In5th International Conference on Mathematical Foundations of Programming Semantics, volume 442 ofLNCS, pages 209-228, 1989.
[24] Paulin-Mohring, C.: ExtractingF ?’s programs from proofs in the Calculus of Constructions. InSixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989.
[25] Paulin-Mohring, C.:Extraction de programmes dans le Calcul des Constructions. PhD thesis, Université Paris VII, 1989.
[26] Paulin-Mohring, C.: Inductive Definitions in the System Coq ? Rules and Properties. InTyped Lambda Calculi and Applications, volume 664 ofLNCS, March 1993. Also in research report 92-49, LIP-ENS Lyon, December 1992.
[27] Poll, E.:A Programming Logic Based on Type Theory. PhD thesis, Technische Universiteit Eindhoven, 1994. · Zbl 0900.03044
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.