CS430/530 Assignment 5
Last modified: October 28, 2013.
Solution posted: November 10, 2013.
Due: Wednesday, November 6, 2013
SF Smallstep
(Please directly modify the abridged Smallstep.v file;
full version at Smallstep.v):
- redo_determinism
- smallstep_bool_shortcut
- properties_of_altered_step: including Coq proofs for the first two questions
- test_multistep_4
- normal_forms_unique
- multistep_congr_2
- eval__multistep
SF Types
(Please directly modify the abridged Types.v file;
full version at Types.v):
- some_term_is_stuck
- finish_progress: formal proof only
- finish_preservation: formal proof only
- subject_expansion: including Coq proofs
SF Stlc
(Please directly modify the abridged Stlc.v file;
full version at Stlc.v):
- substi: inculding substi_correct
- typing_example_3
- typing_nonexample_3
SF StlcProp
(Please directly modify the abridged StlcProp.v file;
full version at StlcProp.v):
- subject_expansion_stlc: including Coq proofs
- type_soundness
- types_unique
Sample Solutions
Sample solutions are on the Zoo machine
/c/cs430/as/as5/{Smallstep,Types,Stlc,StlcProp}-sol.v.