CS430/530 Assignment 5
Last modified: March 5, 2025.
Due: Tuesday, April 1, 2025
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
- step__eval
- multistep__eval
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_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. Note that the question expects a counter example that does not involve conditionals.
- type_soundness
- unique_types