stg-in-coq

Towards a formally verified Haskell compiler

This repository contains things I worked on for my MSc project: first steps towards a Coq-verified compiler for a call-by-need language via the STG machine. The implementation dates back to 2010 (:exclamation:), but it seems there's not been much progress in this direction since then.

Here, you'll find two separate projects:

• stg - results described in my Haskell Symposium 2010 paper: a Coq-verified derivation of the STG machine from a simpler big-step operational semantics,

• vm - results described in my MSc thesis: a Coq-verified compiler from a core calculus to instructions of a virtual machine based on the STG machine (a Haskell version of the compiler was obtained via the Coq extraction mechanism).

⚠️ The code itself does not contain much guidance, but the accompanying papers should suffice to understand what's going on. Also note that everything in this repo was written in a hurry, and I didn't go back to it after I defended the thesis.