Types as abstract interpretations

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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)
Title of host publicationConference Record of the Annual ACM Symposium on Principles of Programming Languages
PublisherACM
Pages316-331
Number of pages16
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

Other

OtherProceedings of the 1997 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'97
CityParis, Fr
Period1/15/971/17/97

Fingerprint

Semantics
Religious buildings
Acoustic waves

ASJC Scopus subject areas

  • Software

Cite this

Cousot, P. (1997). Types as abstract interpretations. In Conference Record of the Annual ACM Symposium on Principles of Programming Languages (pp. 316-331). ACM.

Types as abstract interpretations. / Cousot, Patrick.

Conference Record of the Annual ACM Symposium on Principles of Programming Languages. ACM, 1997. p. 316-331.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cousot, P 1997, Types as abstract interpretations. in Conference Record of the Annual ACM Symposium on Principles of Programming Languages. ACM, pp. 316-331, Proceedings of the 1997 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'97, Paris, Fr, 1/15/97.
Cousot P. Types as abstract interpretations. In Conference Record of the Annual ACM Symposium on Principles of Programming Languages. ACM. 1997. p. 316-331
Cousot, Patrick. / Types as abstract interpretations. Conference Record of the Annual ACM Symposium on Principles of Programming Languages. ACM, 1997. pp. 316-331
@inproceedings{c7537730380b41b0911d126fc7793e55,
title = "Types as abstract interpretations",
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.",
author = "Patrick Cousot",
year = "1997",
language = "English (US)",
pages = "316--331",
booktitle = "Conference Record of the Annual ACM Symposium on Principles of Programming Languages",
publisher = "ACM",

}

TY - GEN

T1 - Types as abstract interpretations

AU - Cousot, Patrick

PY - 1997

Y1 - 1997

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0030681155&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0030681155&partnerID=8YFLogxK

M3 - Conference contribution

SP - 316

EP - 331

BT - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

PB - ACM

ER -