HOME | DEUTSCH | IMPRESSUM | KIT

masters thesis (finished): Formal Verification of Lower Your Guards

Lower Your Guards (LYG) describes static analyses for identifying redundant an incomplete pattern-matching definitions for languages with lazy evaluation, like Hasekell.

Although the implementation of LYG within the Glasgow Haskell Compiler is tested on a huge corpus of Haskell programs, we are still a long way from a correctness proof. To date, there isn't even a formal semantics for the involved intermediate representations that a correctness theorem could be formulated in terms of.

Task:

This work involves coming up with a formal semantics for LYG's guard trees in Lean 3, based on which a correctness theorem should be formulated and subsequently be proven.

Prerequisits

Knowledge of Haskell, General interest in formal proofs, optionally Lean 

Advisors

Scientific Staff
Sebastian Graf

Students

former tutors
Henning Dieterichs