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 theorempure type systemfree theorems

Mathematics Subject Classification ID

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

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)

• A presheaf model of parametric type theory
• scientific article; zbMATH DE number 7559277 (Why is no real title available?)
• Leibniz equality is isomorphic to Martin-Löf identity, parametrically
• Translating dependency into parametricity
• scientific article; zbMATH DE number 7168146 (Why is no real title available?)
• A computational interpretation of parametricity
• Subtyping dependent types
• Integrating linear and dependent types
• Types as parameters
• A unified treatment of syntax with binders
• Proofs for free. Parametricity for dependent types
• Internal parametricity for cubical type theory
• A syntax for higher inductive-inductive types
• Internal diagrams and archetypal reasoning in category theory
• Parametricity in an impredicative sort
• Canonicity and normalization for dependent type theory
• A parametricity-based formalization of semi-simplicial and semi-cubical sets
• Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory

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)