Proofs for free
From MaRDI portal
Publication:2844694
DOI10.1017/S0956796812000056zbMath1271.68076OpenAlexW1664326696MaRDI QIDQ2844694
Patrik Jansson, Jean-Philippe Bernardy, Ross Paterson
Publication date: 19 August 2013
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796812000056
Related Items
Lax Theory Morphisms, Canonicity of weak \(\omega\)-groupoid laws using parametricity theory, Proof-Relevant Parametricity, I Got Plenty o’ Nuttin’, Unnamed Item, Formalizing semantic bidirectionalization and extensions with dependent types, Leibniz equality is isomorphic to Martin-Löf identity, parametrically, The \textsc{MetaCoq} project, A presheaf model of parametric type theory, Friends with Benefits, A Syntax for Higher Inductive-Inductive Types, Ornaments for Proof Reuse in Coq, Is Impredicativity Implicitly Implicit, Comprehensive Parametric Polymorphism: Categorical Models and Type Theory, Pointers in Recursion: Exploring the Tropics
Cites Work
- The Girard-Reynolds isomorphism (second edition)
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- Inductive families
- Free theorems involving type constructor classes
- Parametricity, type equality, and higher-order polymorphism
- The view from the left
- Nameless, painless
- A formulation of the simple theory of types
