Parametricity and dependent types

DOI10.1145/1863543.1863592MaRDI QIDQ5176953zbMATH OpenOpenAlexFDO

Authors Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson

Publication date 5 March 2015

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

Full work available at URL https://research.chalmers.se/en/publication/118913

zbMATH Keywords

abstraction theoremfree theoremspure type system

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Proofs for free. Parametricity for dependent types
• A computational interpretation of parametricity
• A relationally parametric model of dependent type theory
• Formal parametric polymorphism
• Types, abstraction, and parametric polymorphism, part 2

Cited in

(18)

• Canonicity and normalization for dependent type theory
• Integrating linear and dependent types
• Proofs for free. Parametricity for dependent types
• A computational interpretation of parametricity
• A unified treatment of syntax with binders
• Internal diagrams and archetypal reasoning in category theory
• Parametricity in an impredicative sort
• A syntax for higher inductive-inductive types
• Internal parametricity for cubical type theory
• Types as parameters
• Homotopy canonicity for cubical type theory
• Leibniz equality is isomorphic to Martin-Löf identity, parametrically
• Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory
• Translating dependency into parametricity
• Signatures and induction principles for higher inductive-inductive types
• Subtyping dependent types
• A presheaf model of parametric type theory
• A parametricity-based formalization of semi-simplicial and semi-cubical sets

This page was built for publication: Parametricity and dependent types

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