Introduction and Elimination, Left and Right
summary
Claims that four rule choices—right/left introduction and elimination—yield four distinct program structures but are equally expressive through mechanical encodings that never duplicate or discard information, a property called bi-expressibility. Provides formal encodings between diagonally opposed rules, a proof/refutation duality linking proofs and refutations, and a working prototype language Duo prototype that implements producer/consumer terms and an automated “dualize” transform which successfully generates the dual program.
AI-written summary · about
chapters (6)
- 0:00Introduction to typing rules
- 1:11Four types of calculi
- 3:27Program structure examples
- 9:05Formalizing rule systems
- 12:53Proof-refutation duality
- 15:33The Duo language and conclusion
related talks
01h 02mThe Truth of a Procedure
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
26mA Rule-Based Approach for Designing and Composing Abstract Domains
19mThe Logical Essence of Well-Bracketed Control Flow
34mA Taste of Prolog
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
01h 34mFormal Logic Undressed