Internalizing relational parametricity in the extensional calculus of constructions

DOI10.4230/LIPICS.CSL.2013.432MaRDI QIDQ2958537zbMATH OpenFDO

Authors Neelakantan R. Krishnaswami, Derek Dreyer

Publication date 2 February 2017

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2013.432

zbMATH Keywords

dependent typesquasi-PERsrelational parametricity

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• A computational interpretation of parametricity
• A relationally parametric model of dependent type theory
• Internal parametricity for cubical type theory
• A presheaf model of parametric type theory
• Parametricity in an impredicative sort

Cited in

(10)

• Conservativity of nested relational calculi with internal generic functions
• Graded modal dependent type theory
• From realizability to induction via dependent intersection
• Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
• A computational interpretation of parametricity
• Proof-Relevant Parametricity
• Internal parametricity for cubical type theory
• The calculus of dependent lambda eliminations
• A presheaf model of parametric type theory
• Extending equational monadic reasoning with monad transformers

This page was built for publication: Internalizing relational parametricity in the extensional calculus of constructions

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