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 

Publications

Publication

Formal Verification of Pattern Matching Analyses

Advisors

Scientific Staff
Sebastian Graf

Students

former tutors
Henning Dieterichs