Parametricity in an impredicative sort

DOI10.4230/LIPICS.CSL.2012.381zbMATH Open1252.68259arXiv1209.6336MaRDI QIDQ4649560FDOQ4649560

Authors: Chantal Keller, Marc Lasson 

Publication date: 22 November 2012

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

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

zbMATH Keywords

parametricityCoqcalculus of inductive constructionsuniversesimpredicativity

Mathematics Subject Classification ID

Cited In (9)

• The \textsc{MetaCoq} project
• A computational interpretation of parametricity
• A formal proof of the irrationality of \(\zeta(3)\)
• Title not available (Why is that?)
• 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

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)