P. Cousot, Types as Abstract Interpretations

Patrick Cousot.
Types as Abstract Interpretations, invited paper.
In Conference Record of the 24th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming L anguages, Paris, France, 15--17 January 1997. ACM Press, New York, U.S.A. pp. 316-331.
Paper: PDF (460 K)
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 fixpoint 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 à 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.
Slides of the one hour POPL'97 invited talk are available in PDF

\bibitem{Cousot97-1}
P.~Cousot.
\newblock Types as abstract interpretations.
\newblock In \emph{Conference Record of the Twentyfourth Annual ACM
  SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages 316--331, Paris, France, January 1997. ACM Press, New York,
  NY.

@inproceedings{Cousot97-1,
   author =    {Cousot, P{.}},
   title =     {Types as Abstract Interpretations, invited paper},
   pages =     {316--331},
   booktitle = {Conference Record of the Twentyfourth Annual ACM SIGPLAN-SIGACT 
                Symposium on Principles of Programming Languages},
   address =   {Paris, France},
   publisher = {ACM Press, New York, NY},
   month =     jan,
   year =      1997,
}

copyright notice
Last modified: Friday, 04-May-2012 14:01:36 EDT