Proof-Relevant Parametricity

DOI10.1007/978-3-319-30936-1_6zbMath1343.68057OpenAlexW2484548461MaRDI QIDQ3188282

Federico Orsanigo, Neil Ghani, Fredrik Nordvall Forsberg

Publication date: 17 August 2016

Published in: A List of Successes That Can Change the World (Search for Journal in Brave)

Full work available at URL: https://strathprints.strath.ac.uk/64286/

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Universal properties for universal types in bifibrational parametricity

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nonabelian algebraic topology. Filtered spaces, crossed complexes, cubical homotopy groupoids. With contributions by Christopher D. Wensley and Sergei V. Soloviev
• The Girard-Reynolds isomorphism (second edition)
• The calculus of constructions
• On the algebra of cubes
• Fundamental concepts in programming languages
• Proofs for free
• Parametric Polymorphism — Universally
• Two-dimensional models of type theory
• Parametricity and local variables
• Relational Parametricity for Higher Kinds
• A relationally parametric model of dependent type theory
• A presheaf model of parametric type theory
• Bifibrational functorial semantics of parametric polymorphism

This page was built for publication: Proof-Relevant Parametricity