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
- Define system
- Prove Progress
- Prove Preservation
- Add let bindings
- Extend definition
- Prove Progress
- Prove Preservation
- Use the Nominal2 framework to reason about alpha-equated terms
- Add datatypes and
caseexpressions- Extend definition
- Prove Progress
- Prove Preservation
- Extend to System F (ie introduce polymorphic variables)
- Extend definition
- Prove Progress
- Prove Preservation
- Extend System F with Coercions
- Extend definition
- Prove Progress
- Prove Preservation
- TBD
Used literature
Up until now, I mainly used Software Foundations: Programming Language Foundations and the System Fc paper.