Deriving Pretty-Big-Step Semantics from Small-Step Semantics, Mechanised

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.