DeepSpec
 
The Science of Deep Specification
Haskell Core Spec

Haskell Core Spec

The Haskell CoreSpec Project aims to develop formal specifications for a high-level, industrially-relevant functional programming language. In particular, this project targets the core language of the Glasgow Haskell Compiler, the primary compiler for the Haskell programming language. GHC has long been used as both an industrial strength compiler and a platform for language research. The compiler itself is open source, and has primarily been developed and is currently maintained by researchers at Microsoft Research, Cambridge. The CoreSpec project will develop a formal Coq specification of the GHC Core language, including the syntax, type system, and semantics, and connect that specification to other components of the DeepSpec project.

Formalized Haskell project website