Paper: Characterization of typings in polymorphic type discipline (at LICS 1988)
Authors: Paola Giannini Simona Ronchi Della RoccaAbstract
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} }