Title
Semantic parametricity in polymorphic lambda calculus
Abstract
A semantic condition necessary for the parametricity of polymorphic functions is considered. One of its instances is the stability condition for elements of variable type in the coherent domains semantics. A larger setting is presented that does not use retract pairs and keeps intact a basic feature of a certain function-type constructor. Polymorphic lambda terms are semantically parametric because of normalization.<>
Year
DOI
Venue
1988
10.1109/LICS.1988.5126
Edinburgh, UK
Keywords
Field
DocType
data structures,formal logic,coherent domains semantics,function-type constructor,parametricity,polymorphic functions,polymorphic lambda calculus,semantically parametric,stability condition,typed programming languages,variable type
Discrete mathematics,Hindley–Milner type system,Simply typed lambda calculus,Typed lambda calculus,Computer science,System F,Pure mathematics,Church encoding,Pure type system,Parametricity,Dependent type
Conference
Citations 
PageRank 
References 
5
1.50
1
Authors
4
Name
Order
Citations
PageRank
Peter J. Freyd19116.54
Jean-Yves Girard21998370.73
A. Scedrov32108200.16
Philip J. Scott412718.30