A Type Safe Calculus for Generating Syntax-Directed EditorsRemote
Editor calculi make it possible to describe the actions of syntax-directed editing and provide guarantees of safety through their specialized type system: Well-typed editor scripts produce well-formed programs. So far, such calculi have been language-specific. In this paper we present a generalized editor calculus, which can be used to specify a specialized syntax-directed editor for any language, given its abstract syntax. Moreover we show how to implement an editor generator that allows one to generate an editor calculus-based syntax-directed editor from a language specification. The generalized editor calculus can be encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points. This implies a general type safety result that holds for any instantiation.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | High-level abstraction and automationPEPM at Scissors Chair(s): Sam Lindley The University of Edinburgh | ||
09:00 10mDay opening | Welcome PEPM Y. Annie Liu Stony Brook University | ||
09:10 50mKeynote | The Missing Diagonal: High Level Languages for Low Level Systems (Invited Talk Abstract) PEPM Satnam Singh Groq DOI | ||
10:00 30mResearch paper | A Type Safe Calculus for Generating Syntax-Directed EditorsRemote PEPM Andreas Tor Mortensen Department of Computer Science, Aalborg University, Benjamin Bennetzen Department of Computer Science, Aalborg University, Nikolaj Rossander Kristensen Department of Computer Science, Aalborg University, Peter Buus Steffensen Department of Computer Science, Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, Sune Skaanning Engtorp Department of Computer Science, University of Copenhagen DOI |