Parametricity in an impredicative sort

DOI10.4230/LIPICS.CSL.2012.381MaRDI QIDQ4649560zbMATH OpenFDO

Authors Chantal Keller, Marc Lasson

Publication date 22 November 2012

Full work available at URL https://arxiv.org/abs/1209.6336

zbMATH Keywords

parametricityCoqcalculus of inductive constructionsuniversesimpredicativity

Mathematics Subject Classification ID

Recommendations

• A computational interpretation of parametricity
• Proofs for free. Parametricity for dependent types
• Parametricity and dependent types
• A relationally parametric model of dependent type theory
• Relational parametricity for higher kinds

Cited in

(9)

• The \textsc{MetaCoq} project
• A computational interpretation of parametricity
• A formal proof of the irrationality of \(\zeta(3)\)
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• Is Impredicativity Implicitly Implicit
• On the key dependent message security of the Fujisaki-Okamoto constructions
• Internalizing relational parametricity in the extensional calculus of constructions
• The Marriage of Univalence and Parametricity
• Friends with benefits. Implementing corecursion in foundational proof assistants

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Parametricity in an impredicative sort

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