Project Page Index Table of Contents

SysF_PTS.Decidable

SysF_PTS.lib

SysF_PTS.sysf_pts
  • Equivalence of System F and System L in Coq based on Context Morphism Lemmas
    • Traditional System F
    • PTS Syntax
    • System L
    • System P
    • Meta theory of System F
    • PTS properties
    • Meta theory of System P
    • Helpers
    • Equivalence of L and P
    • Equivalence of F and P
    • Preservation of Judgements
    • Cancellation Laws
    • Final Reduction Theorems
Generated by coqdoc and improved by CoqdocJS