Non-parametric parametricity

DOI10.1145/1596550.1596572MaRDI QIDQ2936811zbMATH OpenOpenAlexFDO

Authors Georg Neis, Derek Dreyer, Andreas Rossberg

Publication date 6 January 2015

Published in Proceedings of the 14th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1596550.1596572

zbMATH Keywords

intensional type analysisparametricityrepresentation independencestep-indexed logical relationstype-safe cast

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Non-parametric parametricity
• Parametricity, type equality, and higher-order polymorphism
• Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
• State-dependent representation independence

Cited in

(8)

• Parametricity, type equality, and higher-order polymorphism
• Non-parametric parametricity
• Call-by-name gradual type theory
• State-dependent representation independence
• Generative type abstraction and type-level computation
• Dynamic translucency with abstraction kinds and higher-order coercions
• Type-directed operational semantics for gradual typing
• A logical approach to type soundness

This page was built for publication: Non-parametric parametricity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2936811)