Abstract
This article describes the formalization of the interface of a proof-checker. The latter is based on a kernel consisting of type-checking functions for the Calculus of Constructions, but it seems the ideas can generalize to other type systems, as far as they are based on the proofsas-terms principle. We suppose that the metatheory of the corresponding type system is proved (up to type decidability). We specify and certify the toplevel loop, the system invariant, and the error messages.
Preview
Unable to display preview. Download preview PDF.
References
Barendregt, H.: Lambda Calculi with Types. In Handbook of Logic in Computer Science, Vol II, Elsevier, 1992.
Barras, B.: Coq en Coq. Rapport de Recherche INRIA 3026. Octobre 1996.
Barras, B., Werner, B.: Coq in Coq. Submitted to publication. http://pauillac.inria.fr/~barras/coqincoq.ps.gz
Barras, B., Boutin, S., Cornes, C., Courant, J., Filliâtre, J.-C., Giménez, E., Herbelin, H., Huet, G., Muñoz, C., Murthy, C., Parent, C., Paulin-Mohring, C., Saïbi, A., Werner, B.: The Coq Proof Assistant Reference Manual Version 6.1. Technical Report 0203. Coq Project-INRIA Rocquencourt-ENS Lyon. May 97.
Boyer, R.S., Dowek, G.: Towards Checking Proof-Checkers. In Herman Geuvers, editor, Informal Proceedings of the Nijmegen Workshop on Types for Proofs and Programs, May 1993.
De Bruijn, N.J.: Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Indag. Math. Vol. 34 (5), pp 381–392, 1972.
Coquand, T., Huet, G.: The Calculus of Constructions. In: Information and Computation Vol. 76, February/March 1988 (ed. A.R. Meyer), Academic Press, London, 95–120.
Coscoy, Y., Khan, G., Théry, L.: Extracting text from proofs. INRIA Research Report 2459. January 1995.
Courant, J.: A Module Calculus for Pure Type Systems. In: Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, TLCA'97, Nancy (ed. Ph. de Groote and J. R. Hindley), Springer-Verlag, LNCS 1210, April 1997.
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press.
Geuvers, H., Nederhof, M.-J.: A Modular Proof of Strong Normalization for the Calculus of Constructions. Journal of Functional Programming, 1(2):155–189, April 1991.
Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF: A Mechanized Logic of Computation. Springer-Verlag, LNCS 78, 1979.
Huet, G.: The Constructive Engine. In R. Narasimhan, editor, A Perspective in Theoretical Computer Science. WorldScientific Publishing, 1989. Commemorative Volume for Gift Siromoney.
Leroy, X.: Applicative Functors and Fully Transparent Higher-Order Modules. In: 22nd Symposium on Principles of Programming Languages, pp. 142–153. ACM Press, 1995.
Martin-Löf, P.: A Theory of Types. Technical Report 71-3, University of Stockholm, 1971.
Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in Coq. Journal of Symbolic Computation-special issue on automated programming, 1993.
Pollack, R.: Closure Under Alpha-Conversion. In: Types for Proofs and Programs: International Workshop TYPES'93, Nijmegen, May 1993, Selected Papers, file://ftp.dcs.ed.ac.uk/pub/lego/alpha-closure.ps.gz (ed. H. Barendregt and T. Nipkow), Springer-Verlag, pp. 313–332, LNCS 806, 1994.
Pollack, R.: A Proof Checker for the Extended Calculus of Constructions. Ph. D. Thesis, ftp://ftp.dcs.ed.ac.uk/pub/lego/thesis-pollack.ps.Z University of Edinburgh, 1994.
Pollack, R.: A Verified Typechecker. In: Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, TLCA'95, Edinburgh, (ed. M. Dezani-Ciancaglini and G. Plotkin), Springer-Verlag, LNCS 902, April 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barras, B. (1998). Verification of the interface of a small proof system in coq. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0097785
Download citation
DOI: https://doi.org/10.1007/BFb0097785
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65137-6
Online ISBN: 978-3-540-49562-8
eBook Packages: Springer Book Archive