| START Conference Manager |
Our initial proposal had several limitations. First, it lacked support for recursive types or update procedures. Second, although a high-level source language can easily be translated to the core language, it is difficult to propagate meaningful type errors from the core language back to the source. Third, certain updates are well-formed yet contain path errors, or "dead" subexpressions that never do any useful work. It would be useful to detect path errors, since they often represent errors or optimization opportunities.
In this paper, we address all three limitations. Specifically, we present an improved, sound type system that handles recursion. We also formalize a source update language and give a translation to the core language that preserves and reflects typability. We develop a path-error analysis (a form of dead-code analysis) for updates. We also verify (and in some cases correct) some rewriting rules proposed in earlier work that can be used to optimize core updates.
START Conference Manager (V2.54.6)