Isabelle proving project - Semantics of functional programming languages

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.

Results

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.

Roadmap

• 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)

Used literature

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