Relational Parametricity for a Polymorphic Linear Lambda Calculus

This is the formalism of relational parametricity for PDILL (a term calculus of Polymorphic Dual Intuitionistic Linear Logic), LinF (Linear System F^o) and System F, which has been mechanized using the Coq proof assistant. The code runs with Coq 8.2pl1 (July 2009).

• A proof about the safety of the calculus.
• A proof about open and closed logical relations and parametricity.
• A proof about its soundness and completeness respect to contextual equivalence. and
• A number of applications including empty types, free theorems and type encoding.

• Paper with Tech Report (Aug, 2010) to appear in APLAS 2010
• Tech Report (Jan, 2010)
• Tech Report (Oct, 2009)
• Coq Code
  • README
• Coq Doc
  • Safety and parametricity for PDILL.
  • LinF:
    • Safety for LinF by Steve Zdancewic and Karl Mazurak.
    • Parametricity for LinF.
  • System F:
    • Safety and closed logical relations for CBN System F.
    • Safety and closed logical relations for CBV System F.
    • Safety and open logical relations for CBV System F.
  • Metalib by Brian Aydemir et al.