/coq-undecidability-subtyping

Primary LanguageCoq

Undecidability of Subtyping in System F

Master's thesis of Roberto Alvarez

Dependecies

Installation

Generate makefile with

coq_makefile -f _CoqProject -o Makefile

Then the proof can be compiled and installed with

make
make install

Documentation

The browsable coq code can be found in here.