rodrigogribeiro / unification Public

Notifications You must be signed in to change notification settings
Fork 1
Star 18

Formalisation of a type unification algorithm in Coq proof assistant.

18 stars 1 fork Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 17 Commits
code		code
paper		paper
slides		slides
.gitignore		.gitignore
README.md		README.md

Repository files navigation

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.

About

Formalisation of a type unification algorithm in Coq proof assistant.

Report repository

Releases

No releases published

Packages

No packages published

Languages