ISSN:
1433-299X
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract This paper is an informal introduction to the theory of types which use a connective “∧” for the intersection of two types and a constant “ω” for a universal type, besides the usual connective “→” for function-types. This theory was first devised in about 1977 by Coppo, Dezani and Sallé in the context ofλ-calculus and its main development has been by Coppo and Dezani and their collaborators in Turin. With suitable axioms and rules to assign types toλ-calculus terms, they obtained a system in which (i) the set of types given to a term does not change underλ-conversion, (ii) some interesting sets of terms, for example the solvable terms and the terms with normal form, can be characterised exactly by the types of their members, and (iii) the type-apparatus is not so complex as polymorphic systems with quantifier-containing types and therefore probably not so expensive to implement mechanically as these systems. There are in fact several variant systems with different detailed properties. This paper defines and motivates the simplest one from which the others are derived, and describes its most basic properties. No proofs are given but the motivation is shown by examples. A comprehensive bibliography is included.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01211394
Permalink