A formal proof of "GA = SA"

Cf. EEM
Core language is R.Robert & S.Zdancewic's PrImp.
- In effect based upon Pierce et al's Imp

Name		Name	Last commit message	Last commit date
Latest commit History 45 Commits
docs		docs
.gitignore		.gitignore
LICENSE		LICENSE
Makefile		Makefile
Makefile.coq		Makefile.coq
Makefile.driver		Makefile.driver
README.md		README.md
_CoqProject		_CoqProject
_config.yml		_config.yml
coqdoc.css		coqdoc.css
eng.html		eng.html
eng.v		eng.v
extraction.glob		extraction.glob
extraction.v		extraction.v
extraction.v.d		extraction.v.d
extraction.vo		extraction.vo
imp.cmi		imp.cmi
imp.cmo		imp.cmo
imp.ml		imp.ml
imp.mli		imp.mli
imp1.ml		imp1.ml
imp1.mli		imp1.mli
imp2.ml		imp2.ml
imp2.mli		imp2.mli
impdriver.ml		impdriver.ml
index.html		index.html
lang.v		lang.v
memo.org		memo.org
note.org		note.org
primp1.mli		primp1.mli

Provide feedback