TY - GEN
T1 - Characterization of typings in polymorphic type discipline.
AU - Giannini, Paola
AU - Della Rocca, Simona Ronchi
PY - 1988
Y1 - 1988
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/0024126390
M3 - Conference contribution
AN - SCOPUS:0024126390
SN - 0818608536
T3 - Proc Third Annu Symp on Logic in Comput Sci
SP - 61
EP - 70
BT - Proc Third Annu Symp on Logic in Comput Sci
PB - Publ by IEEE
ER -