Awesome

A Texbook Proof of a Type Unification in Coq

A formalization of a type unification algorithm in Coq.

Structure

• Folder paper/SBMF2015: Source code for SBMF paper.
• Folder paper/SCP: Draft for extended version.
• Folder code/SBMF2015: Coq source code for the formalization of SBMF paper.
• Folder code/SCP: Code for extended version.

Both directories have makefile to build them.