Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

Paper: Type inference and extensionality (at LICS 1994)

Authors: Adolfo Piperno Simona Ronchi della Rocca


The polymorphic type assignment system F2 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 F2 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


    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}