GitHub - felko/anf-fsub: Soundness proof for System F_<: in ANF form

This repository contains a proof for progress and preservation for System F_<: in ANF form.

The proof is based from the POPL '08 tutorial.

Name		Name	Last commit message	Last commit date
Latest commit History 1 Commit
.gitignore		.gitignore
ANF_Definitions.v		ANF_Definitions.v
ANF_Infrastructure.v		ANF_Infrastructure.v
ANF_Lemmas.v		ANF_Lemmas.v
ANF_Soundness.v		ANF_Soundness.v
AdditionalTactics.v		AdditionalTactics.v
Atom.v		Atom.v
Environment.v		Environment.v
FSetDecide.v		FSetDecide.v
FSetNotin.v		FSetNotin.v
FiniteSets.v		FiniteSets.v
ListFacts.v		ListFacts.v
Makefile		Makefile
Makefile.conf		Makefile.conf
Metatheory.v		Metatheory.v
README.md		README.md
_CoqProject		_CoqProject

Provide feedback