Parametricity, type equality, and higher-order polymorphism

DOI10.1017/S0956796810000079zbMath1209.68109MaRDI QIDQ3564921

Stephanie Weirich, Dimitrios Vytiniotis

Publication date: 26 May 2010

Published in: Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (2)

A Reflection on Types ⋮ Proofs for free

Cites Work

• Polytypic values possess polykinded types
• Parametricity and variants of Girard's \(J\) operator
• Type fixpoints
• Syntactic Logical Relations for Polymorphic and Recursive Types
• Non-parametric parametricity
• Free theorems involving type constructor classes
• Typing dynamic typing
• Foundations for structured programming with GADTs
• Free theorems in the presence of seq
• Categories for Types
• Parametric polymorphism and operational equivalence
• FUNCTIONAL PEARL Type-safe cast
• Intensional polymorphism in type-erasure semantics
• Free Theorems and Runtime Type Representations
• On equivalence and canonical forms in the LF type theory
• Fast and loose reasoning is morally correct

This page was built for publication: Parametricity, type equality, and higher-order polymorphism