Nikolai Kudasov: Free Foil: Generating Efficient and Scope-Safe Abstract Syntax

This talk was presented at the 4th International Conference on Code Quality (ICCQ), a one-day computer science event organised in cooperation with the IEEE Russia Section C Chapter and focused on static analysis, program verification, bug detection, and software maintenance. More information about the event you can find on our website: www.iccq.ru/2024.html
Don't hesitate to follow us on Twitter: intent/follow?scr...
If you have any questions or want to contribute to our next events, just email us: [e-mail]
00:00 Start
00:06 Free Foil: Generating Efficient and Scope-Safe Abstract Syntax
00:48 Capture-Avoiding Substitution
02:29 Approaches to Abstract Syntax with Binders
04:33 The Rapier and the Foil
06:41 The Foil: Scope-Safe Types
09:02 The Foil: Sinkability Proof (User Code)
10:11 The Foil: Substitution (User Code)
10:57 Limitations of the Foil
12:28 Distinct Types for Scope Annotation
13:41 The Foil+Template Haskell
14:27 Merging the Foil with Free Scoped Monads
15:18 The Free Foil
15:51 The Free Foil+Template Haskell (experimental)
16:27 Benchmark Results
17:14 Results
17:51 Future work