The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus

DOI10.1016/0304-3975(93)90093-9zbMath0793.03008OpenAlexW2042577486MaRDI QIDQ1314360

Kathleen Milsted, Serguei V. Solov'ev

Publication date: 3 March 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(93)90093-9

zbMATH Keywords

proof theorytype theoryparametricitySystem Fpolymorphic lambda-calculus

Mathematics Subject Classification ID

Theory of programming languages (68N15) Combinatory logic and lambda calculus (03B40)

Related Items

On the power of simple diagrams, POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE, From Applicative to Environmental Bisimulation, A game semantics for generic polymorphism, Building continuous webbed models for system F, Generic type-preserving traversal strategies, Automorphisms of types in certain type theories and representation of finite groups, A full continuous model of polymorphism, Formal parametric polymorphism

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The system \({\mathcal F}\) of variable types, fifteen years later
• A small complete category
• The lambda calculus, its syntax and semantics
• Formal parametric polymorphism
• A generalization of the functorial calculus
• The Category-Theoretic Solution of Recursive Domain Equations
• Constructive natural deduction and its ‘ω-set’ interpretation
• Categorical data types in parametric polymorphism
• A semantic basis for Quest
• Applications of Plotkin-terms: partitions and morphisms for closed terms
• An extension of system F with subtyping