A Fuelled Self-Reducer for System T
summary
Implements a fuelled self-reducer for System T that actually runs: uses Kiselyov and Longley and Normann encodings for products, sums and some inductive types instead of Gödel numerals, producing very large System T terms; proves reduction works given external fuel but System T cannot compute that fuel itself, so termination requires a fuel parameter. Promotes structured encodings into a metalanguage called Primrose compiles into System T, with a verified Idris 2 compiler and ongoing work to make the translation internal.
AI-written summary · about
chapters (9)
- 0:00System T introduction
- 1:07Union and product types
- 2:51Tagged unions in System T
- 4:39Tree depth and root storage
- 6:05Regular types limitations
- 7:31Parallel reduction steps
- 8:32Fueled self-reducer for System T
- 9:59Summary and current work
- 10:34Q&A on System T
related talks
23mProductivity Verification for Functional Programs by Reduction to Termination Ve...
56mOn Type-Based Techniques for Program Manipulation
12mOn the metatheory of IRs and the CPS-calculus
41mType-driven Development of Communicating Systems in Idris
31mDependent tagless final
18mThe Essence of Generalized Algebraic Data Types
14mHigher-order Automation In TLAPS
27mLightweight Semantics Engineering with Redex