% Andrew Appel's solution to List-machine benchmark,
% with proofs (and some auxiliary lemmas) deleted.
machine.elf % Represent the operational semantics
types.elf % Represent the type system, including least-common-supertype alg.
typecheck.elf % Type-checking algorithm
test.elf % Compute executions of SOS, type system, type-checker
unify.elf % State and prove properties of least-common-supertype
specification.elf % state the soundness theorem
proofs.elf % prove the soundness theorem
termination.elf % prove that the type-checker terminates
typecheck-proofs.elf % soundness of type-checker