Lower Your Guards (LYG) beschreibt statische Analysen zur Identifizierung von redundanten und unvollständigen Pattern-Matching Definitionen für Sprachen mit Lazy Evaluation wie Haskell.

Obwohl die Implementierung von LYG im Glasgow Haskell Compiler (GHC) auf einem großen Korpus von Haskell-Programmen getestet wurde, ist das noch kein Beweis für die Korrektheit der implementierten Analysen. Tatsächlich fehlt LYG sogar eine formale Semantik, auf Grundlage der man erst ein Korrektheitsprädikat formulieren kann.

Aufgabe:

In dieser Arbeit soll eine Semantik für Guard Trees aus LYG in Lean 3 formalisiert werden, auf Grundlage der geeignete Korrektheitstheoreme formuliert und schlussendlich bewiesen werden sollen.

Voraussetzungen

Haskell-Kenntnisse, Interesse an formalen Beweisen, evtl. Lean

Schlüsselworte

Haskell, GHC, Lower Your Guards, Formale Verifikation 

Veröffentlichungen

Veröffentlichung

Formal Verification of Pattern Matching Analyses

Betreuer

Wissenschaftliche Mitarbeiter
Sebastian Graf

Studenten

Ehemalige Tutoren
Henning Dieterichs