Introduction to generalized type systems
- 1 April 1991
- journal article
- research article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 1 (2) , 125-154
- https://doi.org/10.1017/s0956796800020025
Abstract
Programming languages often come with type systems. Some of these are simple, others are sophisticated. As a stylistic representation of types in programming languages several versions of typed lambda calculus are studied. During the last 20 years many of these systems have appeared, so there is some need of classification. Working towards a taxonomy, Barendregt (1991) gives a fine-structure of the theory of constructions (Coquand and Huet 1988) in the form of a canonical cube of eight type systems ordered by inclusion. Berardi (1988) and Terlouw (1988) have independently generalized the method of constructing systems in the λ-cube. Moreover, Berardi (1988, 1990) showed that the generalized type systems are flexible enough to describe many logical systems. In that way the well-knownpropositions-as-typesinterpretation obtains a nice canonical form.Keywords
This publication has 14 references indexed in Scilit:
- A Construction of the Provable Wellorderings of the Theory of SpeciesPublished by Springer Nature ,2001
- The calculus of constructionsInformation and Computation, 1988
- On understanding types, data abstraction, and polymorphismACM Computing Surveys, 1985
- Miranda: A non-strict functional language with polymorphic typesLecture Notes in Computer Science, 1985
- A proposal for standard MLPublished by Association for Computing Machinery (ACM) ,1984
- Logic and structure, by D. van Dalen. Pp 180. $13·50. 1980. ISBN 3-540-09893-3 (Springer)The Mathematical Gazette, 1981
- Big trees in a λ-calculus with λ-expressions as typesPublished by Springer Nature ,1975
- Combinatory Logic. By H. B. Curry and R. Feys. Pp. 417. 42s. 1958. (North Holland Publishing Co., Amsterdam)The Mathematical Gazette, 1960
- On the rules of proof in the pure functional calculus of the first orderThe Journal of Symbolic Logic, 1951
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940