Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
summary
An intermediate representation called Xcut intermediate representation encodes classical sequent calculus as a normalized term language with formal typing and a small‑step operational semantics, and a compiler maps it directly to RISC‑V, x86 and ARM machine code. Structural rules become parallel moves or memory ops, negation/continuations and effect handlers are first‑class, and common patterns (result matching vs handler passing) compile to the same indirect‑jump/vtable code with payloads kept in registers so no allocation is necessary — benchmarks without optimizations show viable performance and reproducible artifacts.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:23Xcut intermediate representation
- 1:07Computation as interaction
- 2:11Sequent calculus and cut rule
- 3:39Logical connectives in terms
- 4:46Logic to hardware
- 6:09Error handling with Xcut
- 7:57Unifying data and code
- 9:00Formal definition and codegen
- 10:02Q&A
related talks
31mFormal Specification
30mCalculating Compilers for Concurrency
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
15mMy Journey in Secure Compilation
15mCompiling with Continuations, Correctly
16mS4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
41mThe Dialectics of Type-Level Programming