Logic in Computer Science (LICS 1994)

Paper: Type inference and extensionality (at LICS 1994)

Authors: Adolfo Piperno Simona Ronchi della Rocca

Abstract

The polymorphic type assignment system F₂ is the type assignment counterpart of Girard's and Reynolds' (1972) system F. Though introduced in the early seventies, both the type inference and the type checking problems for F₂ remained open for a long time. Recently, an undecidability result was announced. Consequently, it is considerably interesting to find decidable restrictions of the system. We show a bounded type inference and a bounded type checking algorithm, both based on the study of the relationship between the typability of a term and the typability of terms that “properly” η-reduce to it

BibTeX

  @InProceedings{PipernoRonchidellaR-Typeinferenceandext,
    author = 	 {Adolfo Piperno and Simona Ronchi della Rocca},
    title = 	 {Type inference and extensionality},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994},
    year =	 1994,
    editor =	 {Samson Abramsky},
    month =	 {July}, 
    pages =      {196--205},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }