×

A higher-order calculus and theory abstraction. (English) Zbl 0719.03004

A theory of dependent types, the Extended Calculus of Constructions (ECC), is presented and studied. As a formal system, ECC extends Coquand- Huet’s calculus of constructions with predicative type universes and \(\Sigma\)-types (strong sum); it may also be seen as an extension of Martin-Löf’s type theory with universes by an impredicative universe (higher-order logic). However, different from Martin-Löf’s type theory and the calculus of constructions, the incorporation of both an impredicative universe and predicative universes enhances a conceptual distinction between the notion of logical formulas (propositions) and that of sets (data types). This leads to a unifying theory of dependent types which provides not only a strong logical power but also adequate abstraction mechanisms which, for example, allow comprehensive structuring of development of specifications, programs and proofs. In this paper, after a summary of the proof-theoretic properties of the type theory (strong normalization etc.), a realizability model is described to show how the essential properties of the type system can be captured set- theoretically. The model entails the consistency of the higher-order logic embedded in the theory and also gives some hints on how to formalize abstract mathematics adequately. Abstract reasoning in interactive proof development (based on a notion of abstract theory) is discussed as a pragmatic application.
Recent related work includes the author’s papers “Program specification and data refinement in type theory” [LFCS report ECS-LFCS-91-131, Dept. Comput. Sci., Univ. Edinburgh (1991)] and “A problem of adequacy: conservativity of calculus of constructions over higher-order logic” [LFCS report ECS-LFCS-90-121, Dept. Comput. Sci., Univ. Edinburgh (1990)]; the former develops a type-theoretic approach to program specification and data refinement based on ECC, and the latter proves that the calculus of constructions with type constants is a conservative extension over higher-order predicate logic, which settles a problem left open in this paper.
Reviewer: Z.Luo

MSC:

03B15 Higher-order logic; type theory (MSC2010)
03F35 Second- and higher-order arithmetic and fragments
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Berardi, S., Non-conservativity of Coquand’s calculus with respect to higher-order intuitionistic logic, (talk given in the 3rd Jumelage Meeting on Typed Lambda Calculi. talk given in the 3rd Jumelage Meeting on Typed Lambda Calculi, Edinburgh, Sept. 1989 (1989))
[2] Burstall, R.; Goguen, J., The semantics of CLEAR, a specification language, (Lecture Notes in Computer Science, Vol. 86 (1980), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0456.68024
[3] Burstall, R.; Lampson, B., Pebble, a kernel language for modules and abstract data types, (Lecture Notes in Computer Science, Vol. 173 (1984), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0646.68018
[4] Burstall, R.; Luo, Z., A set-theoretic setting for structuring theories in proof development (1988), circulated notes, April
[5] Burstall, R., Programming with modules as typed functional programming, (Proceedings, Internat. Conf. on Fifth Generation Computer Systems. Proceedings, Internat. Conf. on Fifth Generation Computer Systems, Tokyo (1984))
[6] Burstall, R., Research in interactive theorem proving at Edinburgh University, (Proceedings, 20th IBM Computer Science Symposium. Proceedings, 20th IBM Computer Science Symposium, Shizuoka, Japan. Proceedings, 20th IBM Computer Science Symposium. Proceedings, 20th IBM Computer Science Symposium, Shizuoka, Japan, LFCS Report ECS-LFCS-86-12 (1986), Dept. of Computer Science, University of Edinburgh)
[7] Burstall, R., An approach to program specification and development in constructions, (talk given in Workshop on Programming Logic. talk given in Workshop on Programming Logic, Bastad, Sweden, May (1989))
[8] Cartmell, J., Contextual category and generalized algebraic theories, Ann. Pure Appl. Logic, 32 (1986) · Zbl 0634.18003
[9] Curry, H. B.; Feys, R., (Combinatory Logic, Vol. 1 (1958), North-Holland: North-Holland Amsterdam) · Zbl 0175.27601
[10] Coquand, Th.; Gunter, C.; Winskel, G., Domain Theoretic Models of Polymorphism, (Tech. Report No. 116 (1987), Computer Laboratory, University of Cambridge) · Zbl 0683.03007
[11] Coquand, Th.; Huet, G., Constructions: A higher order proof system for mechanizing mathematics, (EUROCAL ’85. EUROCAL ’85, Lecture Notes in Computer Science, Vol. 203 (1985), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0581.03007
[12] Coquand, Th.; Huet, G., The calculus of constructions, Inform. and Comput., 76, Nos. 2/3, 95-120 (1988) · Zbl 0654.03045
[13] Church, A., A formulation of the simple theory of types, J. Symbolic Logic, 5, No. 1 (1940) · JFM 66.1192.06
[14] Constable, R. L., (Implementing Mathematics with the NuPRL Proof Development System (1986), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ)
[15] Coquand, Th., Une Théorie des Constructions, (Ph.D. thesis (1985), University of Paris VII)
[16] Coquand, Th., An analysis of Girard’s paradox, (Proceedings, 1st Annu. Symp. on Logic in Computer Science (1986))
[17] Coquand, Th., A calculus of constructions (1986), manuscript
[18] Coquand, Th., Metamathematical investigations of a calculus of constructions (1989), manuscript
[19] Coquand, Th.; Paulin, C., Inductively defined types (1989), draft · Zbl 0722.03006
[20] de Bruijn, N. G., A survey of the project AUTOMATH, (Hindley, J.; Seldin, J., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (1980), Academic Press: Academic Press New York) · Zbl 0648.68099
[21] Devlin, K., (Fundamentals of Contemporary Set Theory (1979), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0407.04003
[22] Ehrhard, T., A categorical semantics of constructions, (Proceedings, 3rd Annu. Symp. on Logic in Computer Science. Proceedings, 3rd Annu. Symp. on Logic in Computer Science, Edinburgh (1988))
[23] Geuvers, H., A modular proof of strong normalization for the calculus of constructions, (talk given in the 3rd Jumelage Meeting on Typed Lambda Calculi. talk given in the 3rd Jumelage Meeting on Typed Lambda Calculi, Edinburgh, Sept. 1989 (1989)) · Zbl 1159.03311
[24] Girard, J.-Y., Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur, (thèse (1972), Université Paris VII)
[25] Girard, J.-Y., The system \(F\) of variable types, fifteen years later, Theoret. Comput. Sci., 45 (1986) · Zbl 0623.03013
[26] Hook, J.; Howe, D., (Impredicative Strong Existential Equivalent to Type: Type (1986), Cornell University), Technical Report TR86-760
[27] Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, (Proceedings, 2nd Annu. Symp. on Logic in Computer Science (1987)) · Zbl 0778.03004
[28] Harper, R.; MacQueen, D.; Milner, R., Standard ML, (LFCS Report ECS-LFCS-86-2 (1986), Dept. of Computer Science, University of Edinburgh)
[29] Howard, W. A., The formulae-as-types notion of construction, (Hindley, J.; Seldin, J., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (1980), Academic Press: Academic Press New York)
[30] Hyland, M.; Pitts, A., The theory of constructions: Categorical semantics and topos-theoretic models, (Categories in Computer Science and Logic, Boulder (1987)) · Zbl 0721.03048
[31] Harper, R.; Pollack, R., Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions, Theoret. Comput. Sci. (1989), to appear
[32] Hyland, M., The effective topos, (Troelstra, A. S.; Dalen, Van, The Brouwer Symposium (1982), North-Holland: North-Holland Amsterdam) · Zbl 0522.03055
[33] Hyland, M., A small complete category, Ann. Pure Appl. Logic (1987), to appear · Zbl 0659.18007
[34] Klop, J. W., Combinatory Reduction Systems, (Mathematical Center Tracts, Vol. 127 (1980), Math. Centrum: Math. Centrum Amsterdam) · Zbl 0466.03006
[35] Lampson, B.; Burstall, R., Pebble, a kernel language for modules and abstract data types, Inform. and Comput., 76, Nos. 2/3, 278-346 (1988) · Zbl 0646.68018
[36] Leivant, D., Stratified polymorphism, (Proceedings, Fourth Symp. on Logic in Computer Science. Proceedings, Fourth Symp. on Logic in Computer Science, Asilomar, California (1989)) · Zbl 0716.68019
[37] Levy, A., (Basic Set Theory (1979), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0404.04001
[38] Longo, G.; Moggi, E., (Constructive Natural Deduction and Its ‘Modest’ Interpretation (1988), Computer Science Dept., Carnegie Mellon University), Report CMU-CS-88-131
[39] Luo, Z.; Pollack, R.; Taylor, P., (How to Use LEGO: A Preliminary User’s Manual (1989), LFCS. Dept. of Computer Science, University of Edinburgh)
[40] Luo, Z., (A Higher-Order Calculus and Theory Abstraction (1988), Dept. of Computer Science, University of Edinburgh), LFCS Report ECS-LFCS-88-57
[41] Luo, Z., \(( CC_⊂^∞\) and Its Meta Theory (1988), Dept. of Computer Science, University of Edinburgh), LFCS Report ECS-LFCS-88-58
[42] Luo, Z., ECC, an extended calculus of constructions, (Proceedings, Fourth Annu. Symp. on Logic in Computer Science. Proceedings, Fourth Annu. Symp. on Logic in Computer Science, June 1989, Asilomar, California (1989)) · Zbl 0723.03034
[43] Luo, Z., An extended calculus of constructions, thesis (1989), in preparation · Zbl 0723.03034
[44] MacQueen, D., Using dependent types to express modular structure, (Proceedings, 13th Principles of Programming Languages (1986))
[45] Meseguer, J., (Relating Models of Polymorphism (1988), Computer Science Lab, SRI International), SRI-CSL-88-13
[46] Mitchell, J.; Harper, R., The essence of ML, (Proceedings, 15th Principles of Programming Languages (1988))
[47] Martin-Löf, P., An intuitionistic theory of types (1972), manuscript
[48] Martin-Löf, P., An intuitionistic theory of types: Predicative part, (Rose, H.; Shepherdson, J. C., Logic Colloquium ’73 (1973), Elsevier-North Holland: Elsevier-North Holland New York) · Zbl 0334.02016
[49] Martin-Löf, P., Intuitionistic Type Theory (1984), Bibliopolis, Napoli
[50] Mitchell, J.; Plotkin, G., Abstract types have existential type, (Proceedings, 12th Principles of Programming Languages (1985))
[51] Moggi, E., The PER-model as internal category with all small products (1985), manuscript
[52] Nordström, B.; Petersson, K.; Smith, J., Programming in Martin-Löf’s type theory: An introduction (1990), Oxford University Press: Oxford University Press Oxford · Zbl 0744.03029
[53] Ore, C-E., Notes about the extensions of ECC for including inductive (recursive) types (1989), draft
[54] Paulson, L., (Theorem Proving in Cambridge LCF (1987), Cambridge Univ. Press: Cambridge Univ. Press Cambridge)
[55] Pitts, A., Polymorphism is set theoretic, constructively, (Summer Conf. on Category Theory and Computer Science. Summer Conf. on Category Theory and Computer Science, Edinburgh (1987)) · Zbl 0644.18003
[56] Pollack, R., The theory of LEGO (1989), manuscript
[57] Pottinger, G., (Strong Normalization for Terms of the Theory of Constructions (1987), Odyssey Research Associates), TR 11-7
[58] Prawitz, D., (Natural Deduction, a Proof-Theoretic Study (1965), Almqvist & Wiksells: Almqvist & Wiksells Stockholm)
[59] Reynolds, J. C., Towards a theory of type structure, (Lecture Notes in Computer Science, Vol. 19 (1974), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0219.68044
[60] Reynolds, J. C., Types, abstraction and parameter polymorphism, (Information Processing ’83 (1983))
[61] Reynolds, J. C., Polymorphism is not set-theoretic, (Lecture Notes in Computer Science, Vol. 173 (1984), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0554.03012
[62] Reynolds, J. C.; Plotkin, G. D., (On Functors Expressible in the Polymorphic Typed Lambda Calculus (1988), Dept. of Computer Science, University of Edinburgh), LFCS Report, ECS-LFCS-88-53 · Zbl 0785.03004
[63] Sannella, D.; Burstall, R., Structured theories in LCF, (8th Colloquium on Trees in Algebra and Programming (1983)) · Zbl 0527.68070
[64] Seely, R. A.G., Locally cartesian closed categories and type theory, (Math. Proc. Cambridge Philos. Soc., 95 (1984)) · Zbl 0539.03048
[65] Streicher, T., Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions, Ph.D. dissertation (1988), Passau · Zbl 0684.03025
[66] Tait, W. W., A realizability interpretation of the theory of species, (Parikh, R., Logic Colloquium. Logic Colloquium, Lecture Notes in Computer Science, Vol. 453 (1975), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 1111.03004
[67] Takeuti, G., Proof theory, (Stud. Logic 81 (1975)) · Zbl 0182.01202
[68] Taylor, P.; Luo, Z., Theories, mathematical structures, and strong sums (1988), in preparation
[69] Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, (Lecture Notes in Mathematics, Vol. 344 (1973), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0275.02025
[70] van Daalen, D. T., The Language Theory of Automath, (Ph.D. thesis (1980), Technological University: Technological University Eindhoven) · Zbl 0422.68045
[71] Zucker, J., Formalization of classical mathematics in AUTOMATH, (Colloque Internationaux du CNRS, 249 (1975)), Clermont-Ferrand, France · Zbl 0436.68060
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.