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

calculus of inductive constructionsCoqimpredicativityparametricityuniverses

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

(13)

• The \textsc{MetaCoq} project
• On the key dependent message security of the Fujisaki-Okamoto constructions
• Internalizing relational parametricity in the extensional calculus of constructions
• A computational interpretation of parametricity
• Friends with benefits. Implementing corecursion in foundational proof assistants
• The Marriage of Univalence and Parametricity
• A formal proof of the irrationality of (3)
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• Is Impredicativity Implicitly Implicit
• Parametricity, automorphisms of the universe, and excluded middle
• Bialgebraic reasoning on higher-order program equivalence
• Extending equational monadic reasoning with monad transformers
• Program optimisations via hylomorphisms for extraction of executable code

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)