A type safe calculus for generating syntax-directed editors
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
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 | ||
10:00 30mResearch paper | A type safe calculus for generating syntax-directed editors 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 Skaaning Engtorp Department of Computer Science, University of Copenhagen |