Skip to primary content

PLanCompS

Programming Language Components and Specifications

Main menu

  • Home
  • Background
  • People
  • Publications
  • Semantic descriptions library

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.

Proudly powered by WordPress