Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

Sébastien Carlier, J. B. Wells

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

4 Citations (Scopus)

Abstract

System E is a recently designed type system for the ?-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow implementing the choices via substitution. This paper uses expansion variables in a unification-based automatic type inference algorithm for System E that succeeds for every ß-normalizable ?-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one ß-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and ß-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.

Original languageEnglish
Title of host publicationProceedings of the Sixth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'04
Pages132-143
Number of pages12
Publication statusPublished - 2004
Event14th International Symposium on Logic Based Program Synthesis and Transformation - Verona, Italy
Duration: 26 Aug 200428 Aug 2004

Conference

Conference14th International Symposium on Logic Based Program Synthesis and Transformation
Abbreviated titleLOPSTR 2004
CountryItaly
CityVerona
Period26/08/0428/08/04

Keywords

  • Expansion variables
  • Intersection types
  • Lambda-calculus
  • Type inference

Fingerprint Dive into the research topics of 'Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction'. Together they form a unique fingerprint.

Cite this