System E: Expansion variables for flexible typing with linear and non-linear types and intersection types

Sébastien Carlier, Jeff Polakow, J. B. Wells, A. J. Kfoury

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

11 Citations (Scopus)

Abstract

Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The ! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the ! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with ! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E. © Springer-Verlag 2004.

Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004. Proceedings
Pages294-309
Number of pages16
Volume2986
ISBN (Electronic)978-3-540-24725-8
DOIs
Publication statusPublished - 2004
Event13th European Symposium on Programming - Barcelona, Spain
Duration: 29 Mar 20042 Apr 2004

Publication series

NameLecture Notes in Computer Science
Volume2986
ISSN (Print)0302-9743

Conference

Conference13th European Symposium on Programming
Abbreviated titleESOP 2004
CountrySpain
CityBarcelona
Period29/03/042/04/04

Fingerprint Dive into the research topics of 'System E: Expansion variables for flexible typing with linear and non-linear types and intersection types'. Together they form a unique fingerprint.

  • Cite this

    Carlier, S., Polakow, J., Wells, J. B., & Kfoury, A. J. (2004). System E: Expansion variables for flexible typing with linear and non-linear types and intersection types. In Programming Languages and Systems: 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004. Proceedings (Vol. 2986, pp. 294-309). (Lecture Notes in Computer Science; Vol. 2986). https://doi.org/10.1007/978-3-540-24725-8_21