Proof-Relevant Parametricity
From MaRDI portal
Publication:3188282
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
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)
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)