In this project I want to start with a simply typed lambda calculus, prove type soundness and then extend it step by step until I am at the latest version of System F used in GHC.

You can find the proof of type safety in Soundness.thy, the proof of confluence in Confluence.thy and the determinancy proofs of tying and kinding in Determinancy.thy.

• Start with a simply typed lambda calculus (v1.0)
• Add let bindings (v1.1)
• Use the Nominal2 framework to reason about alpha-equated terms (v2.0)
• Extend to System F (ie introduce polymorphic variables) (v3.0)
• Use a context validity judgement (v3.1)
• Add arbitrary user-defined datatypes (v3.6)
• Add case expressions
• Extend to System Fc (ie introduce type equality coercions)
• Extend to System FcPro (ie introduce kind abstractions)

• Software Foundations: Programming Language Foundations
• System F with type equality coercions.
• Safe zero-cost coercions for Haskell