Realizability and parametricity in pure type systems

DOI10.1007/978-3-642-19805-2_8zbMATH Open1326.68068OpenAlexW2152414370MaRDI QIDQ3000602FDOQ3000602

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

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

Mathematics Subject Classification ID

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

Cited In (6)

• Title not available (Why is that?)
• 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
• A presheaf model of parametric type theory

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)