Hostname: page-component-599cfd5f84-96rnj Total loading time: 0 Render date: 2025-01-07T07:35:25.788Z Has data issue: false hasContentIssue false
  • English
  • Français

Constructive natural deduction and its ‘ω-set’ interpretation†

Published online by Cambridge University Press:  04 March 2009

Giuseppe Longo  and
Eugenio Moggi
Giuseppe Longo
Affiliation:
Laboratoire d'Informatique, CNRS Ecole Normale Superieure, Paris, France
Eugenio Moggi
Affiliation:
LFCS, Computer Science Dept., University of Edinburgh, Edinburgh, UK
Get access Rights & Permissions [Opens in a new window]

Extract

Various Theories of Types are introduced, by stressing the analogy ‘propositions-as-types’: from propositional to higher order types (and Logic). In accordance with this, proofs are described as terms of various calculi, in particular of polymorphic (second order) λ-calculus. A semantic explanation is then given by interpreting individual types and the collection of all types in two simple categories built out of the natural numbers (the modest sets and the universe of ω-sets). The first part of this paper (syntax) may be viewed as a short tutorial with a constructive understanding of the deduction theorem and some work on the expressive power of first and second order quantification. Also in the second part (semantics, §§6–7) the presentation is meant to be elementary, even though we introduce some new facts on types as quotient sets in order to interpret ‘explicit polymorphism’. (The experienced reader in Type Theory may directly go, at first reading, to §§6–8).

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 1 , Issue 2 , July 1991 , pp. 215 - 254
Copyright
Copyright © Cambridge University Press 1991

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Amadio, R., Bruce, K. B. and Longo, G. (1986) The finitary projections model and the solution of higher order domain equations. IEEE Conference on Logic in Computer Science (LICS '86). Boston, 06 1986.Google Scholar
Amadio, R. and Longo, G. (1987) Type-free compiling of parametric types. IFIP Conference on Formal Description of Programming Concepts Ebberup (DK). Wirsing, , ed. North-Holland.Google Scholar
Asperti, A. and Longo, G. (1991) Categories, Types and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT Press.Google Scholar
Bainbridge, E., Freyd, P., Scedrov, A. and Scott, P. J. (1987) Functional Polymorphism. University of Texas Institute on Logical foundations of Functional Programming, Austin.Google Scholar
Barendregt, H., Coppo, M. and Dezani, M. (1983) A filter lambda model and the completeness of type assignment. J. Symb. Logic 48 931–40.Google Scholar
Böhm, C. and Berarducci, A. (1985) Automatic synthesis of typed lambda-programs on term algebras. Theor. Comp. Sci. 39 135–54.CrossRefGoogle Scholar
Breazu-Tannen, V. and Coquand, T. (1987) Extensional models for polymorphism. TAPSOFT-CFLP, Pisa.Google Scholar
Bruce, K. and Longo, G. (1990) Modest models for inheritance and explicit polymorphism. Proc. L.I.C.S. '88, Edinburgh (revised version: Info. & Comp. 87).Google Scholar
Bruce, K., Meyer, A. and Mitchell, J. (1986) The semantics of second order polymorphic lambda-calculus. To appear (Preliminary version: Symposium on Semantics of Data Types). MacQueen, Kahn and Plotkin, , eds, Springer Lecture Notes in Computer Science 173. Springer-Verlag, pp. 131–44.Google Scholar
de Bruijn, N. (1980) A survey of the project AUTHOMATH. In: Hindley, and Seldin, , eds, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism. Academic Press.Google Scholar
Burstall, R. M. and Lampson, B. (1984) A kernel language for abstract data types and modules. In: MacQueen, Kahn and Plotkin, , eds, Symposium on Semantics of Data Types. Springer Lecture Notes in Computer Science 173. Springer-Verlag, pp. 1–50.Google Scholar
Carboni, A., Freyd, P. and Scedrov, A. (1987) A categorical approach to realizability of polymorphic types. 3rd A. C. M. Symp. Math. Found. Progr. Lang. Semantics, Springer Lecture Notes in Computer Science. Springer-Verlag.Google Scholar
Cardelli, L. (1986) A polymorphic lambda-calculus with Type: Type. Preprint, Syst. Res. Center, Dig. Equip. Corp.Google Scholar
Cardelli, L. and Longo, G. (1989) A semantic basis for Quest. Dec-src report 5, 02 1990.Google Scholar
Constable, R. L. et al. (1986) Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall.Google Scholar
Coppo, M. (1984) Completeness of type assignment in continuous lambda-models. Theor. Comp. Sci. 29 309–24.CrossRefGoogle Scholar
Coquand, T. (1985) Une théorie des constructions. Thèse de 3ème cycle, Université Paris VII.Google Scholar
Coquand, T. (1986) An analysis of Girard paradox. IEEE Conference on Longic in Computer Science. Boston, 06 1986.Google Scholar
Coquand, T. and Huet, G. (1985) Constructions: a higher order proof system for mechanizing mathematics. Report 401 INRIA, presented at EUROCAL '85.CrossRefGoogle Scholar
Ehrhard, T. (1988) A categorical semantics of constructions. Proc. L.I.C.S. '88, Edinburgh.Google Scholar
Feferman, X. Y. (1985) A theory of variable types. Rev. Colombiana Matem. XIX 95–105.Google Scholar
Girard, J. Y. (1971) Une extension de l'interpretation de Gödel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la therie des types. In: Festand, J. E., ed, 2nd Scandinavian Logic symposium. North-Holland, pp. 63–92.CrossRefGoogle Scholar
Girard, J. Y. (1972) Interpretation fonctionelle et elimination des coupure dans l'arithmetic d'ordre superieur. Thèse de Doctorat d'Etat, Paris.Google Scholar
Harper, R., Honsell, F. and Plotkin, G. (1987) A framework for defining Logics. L.I.C.S. '87, Cornell, 06 1987.Google Scholar
Hindley, R. (1969) The principal type-scheme of an object in Combinatory Logic. Trans. Amer. Math. Soc. 146 22–60.Google Scholar
Hindley, R. (1983) The completeness theorem for typing lambda-terms. Theor. Comp. Sci. 22 1–17 (also Theoret. Comput. Sci. 22 127–33).Google Scholar
Hindley, R. and Seldin, J. (1986) Introduction to Combinators and Lambda-Calculus. London Mathematical Society.Google Scholar
Huet, G. (1986) Formal structures for computation and deduction. Lecture Notes, C.M.U.Google Scholar
Hyland, M. (1982) The effective Topos. In: Troelstra, and Dalen, Van eds, The Brouwer Symposium. North-Holland.Google Scholar
Hyland, M. (1988) A small complete category. Lecture delivered at the Conference Church's Thesis after 50 years, Zeiss (NL), 06 1986. In: Ann. Pure Appl. Logic 40.Google Scholar
Hyland, M. and Pitts, A. (1987) The theory of constructions: categorical semantics and topos theoretic models. Categories in C.S. and Logic. Boulder (AMS notes).Google Scholar
Hyland, M., Robinson, E. and Rosolini, P. (1987) The discrete objects in the effective topos. Math. Dept., Cambridge University.Google Scholar
Johnstone, P. (1977) Topos Theory. Academic Press.Google Scholar
Knoblock, T. B. and Constable, R. L. (1986) Formalized metareasoning in type theory. IEEE Conference on Logic in Computer Science. Ithaca, 06 1987, pp. 237–48.Google Scholar
Kreisel, G. (1959) Interpretation of analysis by means of constructive functionals of finite type. In: Heyting, A., ed, Constructivity in Mathematics. North-Holland, pp. 101–28.Google Scholar
Lambeck, J. and Scott, P. J. (1980) Intuitionistic type theory and the free topos. J. Pure appl. Algebra 19 215–57.Google Scholar
Longo, G. (1986) On Church's formal theory of functions and functionals. Lecture delivered at the Conference Church's Thesis after 50 years, Zeiss (NL), 06 1986. In: Ann. Pure Appl. Logic 40 93–133.Google Scholar
Longo, G. (1988) From type-structures to type theories, Lecture Notes, Spring semester 1987/1988, C.S. Dept., C.M.U.Google Scholar
Longo, G. and Martini, S. (1986) Computability in higher types, Pω and the completeness of type assignment. Theor. Comp. Sci. 46 2–3 (197–218).CrossRefGoogle Scholar
Longo, G. and Moggi, E. (1990) A category-theoretic characterization of functional completeness. Theor. Comp. Sci. 70, 2 (prelim. version. in Math. Found. Comp. Sci., Prague 1984, Chytil, and Koubek, , eds, Lecture Notes in Computer Science 176. Springer-Verlag, pp. 397–406).Google Scholar
Martin-Löf, P. (1971) A theory of types. Report 71–3, Dept. of Mathematics, University of Stockholm, 02 1971, revised October 1971.Google Scholar
Martin-Löf, P. (1972) An intuitionistic theory of types. Report, Dept. of Mathematics, University of Stockholm, 1972.Google Scholar
Martin-Löf, P. (1975) An intuitionistic theory of types. In: Shepherdson, Rose, ed, Logic Colloquium 73. North-Holland, pp. 73–118.Google Scholar
Martin-Löf, P. (1982) Constructive logic and computer programming. In: Cohen, L. J. et al. , eds, Logic, Methodology and Philosophy of Science VI, North-Holland, pp. 153–75.Google Scholar
Martin-Löf, P. (1984) Intuitionistic Type Theory. Bibliopolis, Napoli.Google Scholar
Meseguer, J. (1988) Relating models of polymorphism. POPL '89.Google Scholar
Meyer, A., Mitchell, J., Moggi, E. and Statman, R. (1987) Empty types in polymorphic lambda calculus. POPL '87.Google Scholar
Milner, R. (1978) A theory of type polymorphism in programming. J. Comput. Sys. Sci. 3 348–75.CrossRefGoogle Scholar
Mitchell, J. (1986) A type-inference approach to reduction properties and semantics of polymorphic expressions. ACM Conference on LISP and Functional Programming. Boston.Google Scholar
Mitchell, J. (1988) Polymorphic type inference and containment. Info. & Comp. 76 (2/3) 211–49.CrossRefGoogle Scholar
Moggi, E. (1986) Messages on ‘Types’. Electronic mailing list.Google Scholar
Moggi, E. (1988) The partial lambda-calculus. PhD Thesis, Edinburgh.Google Scholar
Nederpelt, R. P. (1980) An approach to theorem proving on the basis of a typed lambda calculus. LNCS '87, pp. 182–94.CrossRefGoogle Scholar
Nordstrom, B. (1986) Programming in constructive set theory: some examples. In: Proceedings 1981 Conference on Functional Programming Languages and Computer Architecture. Portsmouth, England, pp. 141–53.Google Scholar
Nordstrom, B. (1961) Martin-Löf type theory as programming logic. Prog. Meth. Group, Rep. 27 Göterborg.Google Scholar
Petersson, K. (1982) A Programming System for Type Theory. Chalmers University, Göteborg.Google Scholar
Pitts, A. (1987) Polymorphism is Set Theoretic, constructively. In: Pitt, et al. , eds. Symposium on Category Theory and Comp. Sci. Springer Lecture Notes in Computer Science 283. Edinburgh.Google Scholar
Plotkin, G. (1977) LCF as a programming language. Theoret. Comput. Sci. 5 223–57.Google Scholar
Reynolds, J. (1984) Polymorphism is not set-theoretic. In: MacQueen, Kahn and Plotkin, , eds, Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173. springer-Verlag.Google Scholar
Reynolds, J. C. (1985) Three approaches to type structures. Lecture Notes in Computer Science 185 145–6.Google Scholar
Retnolds, J. C. and Plotkin, G. (1988) On functors expressible in the polymorphic typed lambda calculus. Preliminary report. C.M.U.Google Scholar
Robinson, E. (1989) How complete is PER? LICS'89.Google Scholar
Rosolini, G. (1986) About modest sets. Notes for a talk delivered in Pisa.Google Scholar
Scott, D. (1970) Constructiver validity. In: Symposium on Automatic Demonstration, Lecture Notes in Mathematics 125, Springer-Verlag, New york, pp. 237–75.CrossRefGoogle Scholar
Scott, D. (1972) Continuous lattices. Toposes, Algebraic Geometry and Logic. Lavwere, , ed, SLNM 274, Springer-Verlag, pp. 97–136.Google Scholar
Scott, D. (1976) Data types as lattices. SIAM J. Comput. 5 522–87.Google Scholar
Scott, D. (1980a) Lambda-calculus, some models, some philosophy. In: Barwise, et al. , eds, The Kleene Symposium. North-Holland.Google Scholar
Seely, R. A. G. (1986) Categorical semantics for higher order polymorphic lambda calculus. JSL 54(4) 969–89.Google Scholar
Taylor, P. (1986) Recursive domains, indexed category theory and polymorphism. PhD Thesis, Imperial College, London.Google Scholar
Troesltra, A. S. (1973) Notes in intuitionistic second-order arithmetic. Cambridge Summer School in Math. Logic, Springer Lecture Notes in Mathematics 337, pp. 171–203.Google Scholar