This page contains the Coq development of the theories and proof of correctness for the derivations in Deriving Pretty-Big-Step Semantics from Small-Step Semantics.
Pretty-printed Coq sources:
- sect_2_4_small_step_lambda
- sect_3_1_small_step_lambda
- sect_3_2_small_step_lambda_refocus
- sect_4_side_effects
A zip containing the Coq sources. Requires Coq ≥ 8.4pl2.