Realizability and parametricity in pure type systems

DOI10.1007/978-3-642-19805-2_8MaRDI QIDQ3000602zbMATH OpenOpenAlexFDO

Authors Jean-Philippe Bernardy, Marc Lasson

Publication date 19 May 2011

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19805-2_8

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Proofs for free. Parametricity for dependent types
• scientific article; zbMATH DE number 512792
• scientific article; zbMATH DE number 2086242
• scientific article; zbMATH DE number 1183239
• scientific article; zbMATH DE number 2185725

Cited in

(6)

• A presheaf model of parametric type theory
• scientific article; zbMATH DE number 2086242 (Why is no real title available?)
• The calculus of dependent lambda eliminations
• On completeness and parametricity in the realizability semantics of System \textsf{F}
• Proofs for free. Parametricity for dependent types
• Controlling Program Extraction in Light Logics

Describes a project that uses

Uses Software

• LCF
• Automath

This page was built for publication: Realizability and parametricity in pure type systems

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