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

Logic in computer science (03B70) Theory of programming languages (68N15) 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

(9)

• Proofs for free. Parametricity for dependent types
• Controlling Program Extraction in Light Logics
• scientific article; zbMATH DE number 2086242 (Why is no real title available?)
• On completeness and parametricity in the realizability semantics of System \textsf{F}
• The calculus of dependent lambda eliminations
• A presheaf model of parametric type theory
• A parametricity-based formalization of semi-simplicial and semi-cubical sets
• A weakly initial algebra for higher-order abstract syntax in Cedille
• Systematic translation of formalizations of type theory from intrinsic to extrinsic style

Describes a project that uses

Uses Software

• Automath
• LCF

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)