Types as abstract interpretations

Research output: Contribution to journalConference article

Abstract

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 languageEnglish (US)
Pages (from-to)316-331
Number of pages16
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
DOIs
StatePublished - 1997
EventProceedings of the 1997 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'97 - Paris, Fr
Duration: Jan 15 1997Jan 17 1997

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Types as abstract interpretations'. Together they form a unique fingerprint.

  • Cite this