The coherence of languages with intersection types

authors: John C Reynolds
year: 1991
url: http://dx.doi.org/10.1007/3-540-54415-1₇0
publisher: Springer Berlin Heidelberg
abstract: When a programming language has a sufficiently rich type structure, there can be more than one proof of the same typing judgement; potentially this can lead to semantic ambiguity since the semantics of a typed language is a function of such proofs. When no such ambiguity arises, we say that the language is coherent. In this paper we prove the coherence of a class of lambda-calculus-based languages that use the intersection type discipline, including both a purely functional programming language and the Algol-like programming language Forsythe.