Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
summary
Proposes Computation-Tree Semantics where configurations are trees that encode evaluation contexts and continuations, making semantic rules algorithmic rather than purely declarative. Converts big-step definitions for a simple arithmetic language, a while language, and Launchbury’s call-by-need lambda calculus into CTS, formalises the arithmetic example in Coq/Rocq, and proves equivalence for those three cases. Implements strict evaluation ordering, supports parallelism and nondeterminism but currently forbids shared-state interaction; aims to automate conversion and extract implementations.
AI-written summary · about
chapters (14)
- 0:00Computation tree semantics intro
- 1:06Big step vs small step semantics
- 3:35Computation trees as core data
- 6:45Step-by-step CTS evaluation
- 9:59CTS vs big step correspondence
- 11:43Big step to CTS conversion
- 13:08Lambda calculus conversion example
- 15:19While language CTS conversion
- 17:08Proving CTS equivalence
- 19:37CTS for type inference
- 20:41Parallelism and nondeterminism in CTS
- 21:24CTS features summary
- 22:07Future CTS automation
- 23:13Q&A
related talks
24mChoice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C...
15mStable Relations and Abstract Interpretation of Higher-Order Programs
15mCompiling with Continuations, Correctly
23mFrom Semantics to Syntax: A Type Theory for Comprehension Categories
01h 06mVerifying a compiler through equational means
32mTyped Program Analysis Without Encodings
30mCalculating Compilers for Concurrency
13mCompiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation