A Functional Abstraction of Typed Trails + A Text-based Syntax Completion Method
summary
Presents a new type system that models continuation invocation contexts as functional trails so control and prompt can have heterogeneous trail types it claims this accepts examples the old system rejects proves termination for the calculus and ships an implementation on GitHub showing the idea works; key technical moves are a CPS translation that passes explicit trail types and a compatibility relation that types trail composition. Proposes a grammar driven completion algorithm using the Yapb error parser that computes finite simple candidates and potentially infinite nested candidates prunes cycles heuristically and demos an Emacs mode that returns sensible completions though it currently ignores text after the cursor.
AI-written summary · about
chapters (23)
- 0:00Introduction
- 1:07Welcome
- 3:38Functional abstraction of typed trails
- 5:23Control and prompt operators
- 10:21Type system design
- 13:21Trail type modification
- 15:09Prompt and control typing rules
- 23:26Type system properties
- 26:24Summary and future directions
- 26:49Q&A on control/prompt
- 32:08Transition to syntax completion
- 33:12Syntax completion overview
- 34:40Algorithm objectives
- 36:51Postfix sentential forms
- 39:04Simple candidates
- 41:37Simple candidates example
- 43:26Nested candidates
- 45:37Nested candidates algorithm
- 50:02Handling infinite candidates
- 51:57Demo of syntax tool
- 53:30Related work
- 56:30Q&A on syntax method
- 1:00:08Closing remarks
related talks
20mAn Approach to Generate Text-Based IDEs for Syntax Correction based on Syntax Specification
17mFrom Traces to Program Incorrectness: A Type-Theoretic Approach
24mA Big-Step Compositional Continuation-Passing Semantics for WebAssembly
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
18mThe Ultimate Conditional Syntax
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
15mBack to Direct Style: Typed and Tight
08mLightning Talk: Designing a Language for Learning Continuations