View source for Publications/carlier.02.itrs

{{Publication
| published = true
| date = 2002-07-01
| authors = Sébastien Carlier
| title = Polar type inference with intersection types and ω
| 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
| address = Copenhagen, Denmark
| lrdeprojects = Software
| 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.
| lrdepaper = http://www.lrde.epita.fr/dload/papers/carlier.02.itrs.pdf
| lrdekeywords = Software engineering
| type = inproceedings
| id = carlier.02.itrs
| bibtex = 
@InProceedings<nowiki>{</nowiki>	  carlier.02.itrs,
  author	= <nowiki>{</nowiki>S\'ebastien Carlier<nowiki>}</nowiki>,
  title		= <nowiki>{</nowiki>Polar type inference with intersection types and $\omega$<nowiki>}</nowiki>,
  booktitle	= <nowiki>{</nowiki>Proceedings of the 2nd Workshop on Intersection Types and
		  Related Systems (ITRS), published in: Electronic Notes in
		  Theoretical Computer Science<nowiki>}</nowiki>,
  volume	= 70,
  issue		= 1,
  publisher	= <nowiki>{</nowiki>Elsevier<nowiki>}</nowiki>,
  year		= 2002,
  address	= <nowiki>{</nowiki>Copenhagen, Denmark<nowiki>}</nowiki>,
  month		= jul,
  abstract	= <nowiki>{</nowiki>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.<nowiki>}</nowiki>
<nowiki>}</nowiki>

}}