Proof-Relevant Parametricity

DOI10.1007/978-3-319-30936-1_6zbMATH Open1343.68057OpenAlexW2484548461MaRDI QIDQ3188282FDOQ3188282

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/

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

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

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)