1991/04/01 by Henk Barendregt · 2 citations
Computer Science · Mathematics · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Formal Methods in Verification #Computer science #Type (biology) #Lambda calculus #Representation (politics) #Cube (algebra) #Interpretation (philosophy) #Programming language #Type theory #Artificial intelligence #Algebra over a field #Theoretical computer science #Mathematics #Pure mathematics #Combinatorics
paper · pdf · doi:10.1017/s0956796800020025
openalex publication_date 1991/04/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/04
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-known propositions-as-types interpretation obtains a nice canonical form.