Title :
Characterization of typings in polymorphic type discipline
Author :
Giannini, Paola ; Rocca, Simona Ronchi Della
Author_Institution :
Dipartimento di Inf., Torino Univ., Italy
Abstract :
Polymorphic type discipline for lambda -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.<>
Keywords :
formal logic; functionality theory; lambda -calculus; polymorphic type discipline; substitutions; typings characterisation; Constraint theory;
Conference_Titel :
Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
Conference_Location :
Edinburgh, UK
Print_ISBN :
0-8186-0853-6
DOI :
10.1109/LICS.1988.5101
