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.