Starting from a denotational semantics of the eager untyped lambda-calculus with explicit runtime errors, the standard collecting semantics is defined as specifying the strongest program properties. By a first abstraction, a new sound type collecting semantics is derived in compositional fix-point form. Then by successive (semi-dual) Galois connection based abstractions, type systems and/or type inference algorithms are designed as abstract semantics or abstract interpreters approximating the type collecting semantics. This leads to a hierarchy of type systems, which is part of the lattice of abstract interpretations of the untyped lambda-calculus. This hierarchy includes two new a la Church/Curry polytype systems. Abstractions of this polytype semantics lead to classical Milner/Mycroft and Damas/-Milner polymorphic type schemes, Church/Curry monotypes and Hindley principal typing algorithm. This shows that types are abstract interpretations.
|Original language||English (US)|
|Number of pages||16|
|Journal||Conference Record of the Annual ACM Symposium on Principles of Programming Languages|
|State||Published - 1997|
|Event||Proceedings of the 1997 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'97 - Paris, Fr|
Duration: Jan 15 1997 → Jan 17 1997
ASJC Scopus subject areas