Theorems proved

There are 2 threorems: progress and preservation.

Progress

The progress theorem is defined in progress.v. It is Theorem 2 from the published article.

There are things missing: In the progress theorem we have

|- H : * completely defined in heap.v as Heap_ok.

H |- F : s completely defined in wf_env.v as WF_Frame

H ; a |- F ok not at all defined.

Except for proving the progress of H ; a |- F ok, the proof is done (all the admits are in preservation).

Same as above, the separation and ocap properties are not defined and not part of the theorem statement. There are admits in the assign case.

The proof of single-frame preservation is finished, except for the two admitted parts (which are the most tricky...)

It doesn't look like preservation_unfixed.v or anything else has preservation for frame stacks.

Name		Name	Last commit message	Last commit date
Latest commit History 35 Commits
.gitignore		.gitignore
README.md		README.md
classTable.v		classTable.v
classTable_orig.v		classTable_orig.v
fs_preservation.v		fs_preservation.v
globals.v		globals.v
heap.v		heap.v
makefile		makefile
namesAndTypes.v		namesAndTypes.v
ocap.v		ocap.v
partial.v		partial.v
preservation.v		preservation.v
preservation_fix.v		preservation_fix.v
preservation_unfixed.v		preservation_unfixed.v
progress.v		progress.v
progress_sf.v		progress_sf.v
reductions.v		reductions.v
sframe.v		sframe.v
syntax.v		syntax.v
typing.v		typing.v
wf_env.v		wf_env.v
wf_env_orig.v		wf_env_orig.v