Undecidability of Subtyping in System F

Master's thesis of Roberto Alvarez

Dependecies

Generate makefile with

coq_makefile -f _CoqProject -o Makefile

Then the proof can be compiled and installed with

make
make install

The browsable coq code can be found in here.

Name		Name	Last commit message	Last commit date
Latest commit History 2 Commits
Reductions		Reductions
Utils		Utils
extras		extras
CM2.v		CM2.v
CM2_undec.v		CM2_undec.v
Fsub.v		Fsub.v
FsubD.v		FsubD.v
FsubD_undec.v		FsubD_undec.v
FsubF.v		FsubF.v
FsubF_undec.v		FsubF_undec.v
FsubN.v		FsubN.v
FsubN_undec.v		FsubN_undec.v
Fsub_na.v		Fsub_na.v
Fsub_na_undec.v		Fsub_na_undec.v
Fsub_undec.v		Fsub_undec.v
README.md		README.md
RM.v		RM.v
RM_undec.v		RM_undec.v
_CoqProject		_CoqProject