Proof-Relevant Parametricity

DOI10.1007/978-3-319-30936-1_6MaRDI QIDQ3188282zbMATH OpenOpenAlexFDO

Authors Neil Ghani, Fredrik Nordvall Forsberg, Federico Orsanigo

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)

Recommendations

• Proofs in parameterized specifications
• Parameterized provability in equational logic
• Paramodulation-based theorem proving
• Parameterized proof complexity
• scientific article; zbMATH DE number 3880082
• A proof-theoretic semantics for parametric logical constants
• Proof relevant corecursive resolution
• Proof and canonical proof
• The power of parameterization in coinductive proof

Cites work

• A presheaf model of parametric type theory
• A relationally parametric model of dependent type theory
• Bifibrational functorial semantics of parametric polymorphism
• Fundamental concepts in programming languages
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• Internalizing relational parametricity in the extensional calculus of constructions
• Nonabelian algebraic topology. Filtered spaces, crossed complexes, cubical homotopy groupoids. With contributions by Christopher D. Wensley and Sergei V. Soloviev
• On the algebra of cubes
• Parametric Polymorphism — Universally
• Parametricity and local variables
• Proofs for free. Parametricity for dependent types
• Relational parametricity for higher kinds
• The calculus of constructions
• The Girard-Reynolds isomorphism (second edition)
• The role of symmetries in cubical sets and cubical categories. (On weak cubical categories. I)
• Two-dimensional models of type theory

Cited in

(4)

• A simple proof technique for certain parametricity results
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
• Universal properties for universal types in bifibrational parametricity
• From parametricity to conservation laws, via Noether's theorem

This page was built for publication: Proof-Relevant Parametricity

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