On Type-Based Techniques for Program Manipulation

on YouTube ↗56m

" summary

Type-directed transformations formalize program rewrites as typing judgments and prove soundness by preservation under reduction plus soundness for values. Two concrete techniques appear: a useless variable elimination that replaces irrelevant subterms with unit via type inference (then removes units) and an intersection-type transformation that compiles a deterministic transducer into a new lambda that maps compressed functional data to outputs. A prototype gtx2 generates OCaml programs (example: it computes 610 occurrences of "ab" in the 16th Fibonacci word). Tools: type inference, intersection types, CPS/tupling for verification.

AI-written summary · about

" chapters (15)

1. 0:00Intro
2. 3:48Type-Based Transformation: Some Common Principles
3. 6:33Outline + Type Based Program Transformation
4. 6:51Useless Variable Elimination (UVE, a.k.a. Useless Code Elimination)
5. 13:15Type Inference Type-Based Transformation
6. 18:35Functional Programs as Compressed Data [K+, PEPM 2012]
7. 20:18Transformation of Compressed Data (without Decompression) word w
8. 21:27Type-based Program Transformation
9. 24:40Type-based Transformation Rules
10. 29:46Demo: Counting "ab" in a Fibonacci word
11. 35:27Outline Type Based Program Transformation
12. 35:44Growing Role of Program Transformation for Trustworthy Computing
13. 36:55Examples of Program Transformations Used for Verification CPS transformation
14. 38:06Tuping Transformation for Relational Reasoning about Functional Programs Asadar, PEPM15
15. 42:10Type-Based Techniques for Formal Languages

" related talks

• 28mType-directed Program Transformation for Constant-Time EnforcementThomas P. Jensen, Frédéric Besson, Gautier Raimondi · PPDP 2023
• 19mIll-Typed Programs Don't EvaluateSteven Ramsay, Charlie Walpole · POPL 2024
• 17mFrom Traces to Program Incorrectness: A Type-Theoretic ApproachJulia Belyakova, Zhe Zhou, Suresh Jagannathan, Benjamin Delaware, Yongwei Yuan · TPSA 2025
• 27mTowards Type Debugging using Partial EvaluationKanae Tsushima, Robert Glück · PEPM 2023
• 21mPolymorphic Type Inference for Dynamic LanguagesKim Nguyen, Giuseppe Castagna, Mickaël Laurent · POPL 2024
• 20mGenerating Well-Typed Terms that are not "Useless"Leonidas Lampropoulos, Justin Frank, Benjamin Quiring · POPL 2024
• 41mThe Dialectics of Type-Level ProgrammingAaron Levin · Lambda World 2016
• 21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)Cunyuan Gao, Lionel Parreaux · GPCE 2024