Awesome

W-in-Coq

This is a Coq formalization of Damas-Milner type system and its algorithm W.

Correctness (soundness) and completeness of W have been proved.

This work is strongly based on Catherine Dubois paper "Certification of a Type Inference Tool for ML: Damas-Milner within Coq". But, in contrast, I decided to use LTac automation, dependent types and a modification of "The Hoare State Monad".

Also, this work uses a modified version of the unification in Coq by Rodrigo Ribeiro. More information about his unification in "A Mechanized Textbook Proof of a Type Unification Algorithm".

The extracted code is fully executable and can be found in the src/extraction folder.

To compile the Coq code run make in the root folder.

To compile the extraced code run stack build in src/extraction folder.

Note: This is a work in progress! Some parts are still quite messy!

Tested with coq 8.9.0.