Logic in Computer Science (LICS 1988)

Paper: Characterization of typings in polymorphic type discipline (at LICS 1988)

Authors: Paola Giannini Simona Ronchi Della Rocca

Abstract

Polymorphic type discipline for λ-calculus is an extension of H.B. Curry's (1969) classical functionality theory, in which types can be universally quantified. An algorithm that, given a term M, builds a set of constraints, is satisfied. Moreover, all the typings for M (if any) are built from the set of constraints by substitutions. Using the set of constraints, some properties of polymorphic type discipline are proved

BibTeX

  @InProceedings{GianniniDellaRocca-Characterizationoft,
    author = 	 {Paola Giannini and Simona Ronchi Della Rocca},
    title = 	 {Characterization of typings in polymorphic type discipline},
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {61--70},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }