TEAL: a Total Expressive Assembly Language
summary
Design of a typed assembly language called TEAL claims total correctness: well-typed programs both terminate and return the specified source-level value. The model is a typed SECD machine whose instruction typing tracks concrete source-language terms so typing rules double as an interpreter. The talk presents mechanized metatheory: type safety and a termination proof via logical relations, yields total correctness for the core calculus, but no implementation yet and the design is still early stage.
AI-written summary · about
chapters (9)
- 0:00TEAL introduction
- 1:24Source and target languages
- 3:09SECD machine explained
- 5:18Type system for instructions
- 7:03Type system modeling computation
- 9:11Type safety guarantees
- 11:37Termination properties
- 13:01TEAL extensions and limits
- 14:28Conclusion and Q&A
related talks
33mTeIL: a type-safe imperative Tensor Intermediate Language
12mSEALS: A framework for building Self-Adaptive Virtual Machines
46mThe Calculated Typer (Functional Pearl)
19mIll-Typed Programs Don't Evaluate
29mA type safe calculus for generating syntax-directed editors
22mA Dependent Language with Type-Safe Program Extraction
09mRetargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
23mTACAI: An Intermediate Representation based on Abstract Interpretation