%  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