A Type-Safe Structure Editor Calculus

Structure editors make syntax errors impossible, but they still allow construction of programs with incomplete semantics, leading to program states that cannot be evaluated. We introduce a structure editor calculus for a simple functional programming language that allows for incomplete programs. Our editor expressions may interleave construction and evaluation of programs and can thus describe the history of the development of a program. We extend our editor calculus with types and define a resource-aware type system that prohibits editor expressions introducing type errors in the abstract syntax tree and prove that the type system is sound.