Polar type inference with intersection types and ω
From LRDE
- Authors
- Sébastien Carlier
- Where
- Proceedings of the 2nd Workshop on Intersection Types and Related Systems (ITRS), published in: Electronic Notes in Theoretical Computer Science
- Place
- Copenhagen, Denmark
- Type
- inproceedings
- Publisher
- Elsevier
- Projects
- Software"Software" is not in the list (Vaucanson, Spot, URBI, Olena, APMC, Tiger, Climb, Speaker ID, Transformers, Bison, ...) of allowed values for the "Related project" property.
- Keywords
- Software engineering
- Date
- 2002-07-01
Abstract
We present a type system featuring intersection types and omega, a type constant which is assigned to unused terms. We exploit and extend the technology of expansion variables from the recently developed System I, with which we believe our system shares many interesting properties, such as strong normalization, principal typings, and compositional analysis. Our presentation emphasizes a polarity discipline and shows its benefits. We syntactically distinguish positive and negative types, and give them different interpretations. We take the point of view that the interpretation of a type is intrinsic to it, and should not change implicitly when it appears at the opposite polarity. Our system is the result of a process which started with an extension of Trevor Jim's Polar Type System.
Documents
Bibtex (lrde.bib)
@InProceedings{ carlier.02.itrs, author = {S\'ebastien Carlier}, title = {Polar type inference with intersection types and $\omega$}, booktitle = {Proceedings of the 2nd Workshop on Intersection Types and Related Systems (ITRS), published in: Electronic Notes in Theoretical Computer Science}, volume = 70, issue = 1, publisher = {Elsevier}, year = 2002, address = {Copenhagen, Denmark}, month = jul, abstract = {We present a type system featuring intersection types and omega, a type constant which is assigned to unused terms. We exploit and extend the technology of expansion variables from the recently developed System I, with which we believe our system shares many interesting properties, such as strong normalization, principal typings, and compositional analysis. Our presentation emphasizes a polarity discipline and shows its benefits. We syntactically distinguish positive and negative types, and give them different interpretations. We take the point of view that the interpretation of a type is intrinsic to it, and should not change implicitly when it appears at the opposite polarity. Our system is the result of a process which started with an extension of Trevor Jim's Polar Type System.} }