A type safe calculus for generating syntax-directed editors
summary
A generalized editor calculus is presented that guarantees that well-typed editor scripts produce well-formed programs by encoding the calculus into a simply typed lambda calculus with pairs, booleans, pattern matching and fixed points; the encoding yields a general type safety proof that applies to any language instantiation. An editor generator in Elm uses code generation (not a generic model) to produce working editors — demonstrated on three languages (C, SQL, TeX) — though context-sensitive syntax and multiple views remain unimplemented.
AI-written summary · about
chapters (8)
- 0:00Type safe structure editors
- 3:54Research highlights
- 6:44Generalized editor calculus
- 14:58Calculus in typed Lambda
- 16:01Editor implementation
- 20:38Example languages editors
- 21:20Conclusion and future work
- 22:09Q&A
related talks
01h 00mA Type-Safe Structure Editor Calculus + Strictly Capturing Non-Strict Closures
22mType-Safe Code Generation With Algebraic Effects and Handlers
19mFlexible Structure Editing of Well-Typed Expressions
46mThe Calculated Typer (Functional Pearl)
24mScoped and Typed Staging by Evaluation
20mAn Approach to Generate Text-Based IDEs for Syntax Correction based on Syntax Specification
19mIll-Typed Programs Don't Evaluate
14mA dependently typed calculus with pattern matching and erasure inference