On the power of syntactic methods: It is all syntax after all…
summary
Argues that many tricky operational problems become simple once the store and sharing are treated as syntax, demonstrates a concrete binding in evaluation contexts trick that captures variables in contexts, and introduces a watermark technique to observe sharing for call-by-need. Formalizes GHC-like intermediate language by expanding terms to infinite normal forms, proves correctness using a small domain-specific proof tool that automates otherwise tedious syntactic proofs, and reports that the automation scales to realistic proofs.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:46Syntactic methods with Cena
- 3:12Cena’s call-by-need proof
- 5:00Cyclic lambda calculus complexity
- 6:23GHC intermediate language work
- 8:09Automating syntax proofs
- 9:14Lambda calculi and natural deduction
- 10:57Favorite papers with Cena
- 11:19PLS summer school contribution
related talks
02h 50mIntro to Type Systems and Operational Semantics
01h 05mAll the Languages Together
48mOpening Keynote
46mRefinement Types from Light to Deep Verification
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
18mThe Ultimate Conditional Syntax
40mFormal semantics for multi-language programs
24mTowards a Higher-Order Mathematical Operational Semantics