arXiv subjects

Thomas J. Porter

Publications and source records attributed to Thomas J. Porter.

3 recordsLinked to original sources

arXiv2026

Incremental Live Programming via Shortcut Memoization

Live programming systems aim to quickly show programmers the dynamic impacts of program edits. To do so, they re-execute the program whenever it is edited, which poses a computational challenge when programs become large or complex. This has led to the need for incrementality in the implementation of live program interpreters. This paper introduces Chordata, an incremental program interpreter based on shortcut memoization, which learns repeated patterns of computation, called shortcuts, by observing executions of previous versions of a program. It can then apply these shortcuts when the same or a structurally similar program fragment is re-executed. This paper contributes a formal semantics of shortcut memoization for any language with a rewrite-based semantics, with mechanized proofs of key correctness properties. We then express a variant of the Hazel live programming system, expressed as a CEK machine, in Chordata, and develop a number of practical heuristics to learn high-value shortcuts. We evaluate the resulting system on editing traces of students solving simple programming problems. Chordata achieves a speedup of 13.03\times compared to baseline with a 19.97\times memory overhead. For smaller changes and for more complex programs, Chordata achieves even greater speedups. Furthermore, we show that Chordata is capable of providing a speedup even within a single execution, with a faster speedup on a larger input.

cs.PL↗

arXiv2025

Syntactic Completions with Material Obligations

Code editors provide essential services that help developers understand, navigate, and modify programs. However, these services often fail in the presence of syntax errors. Existing syntax error recovery techniques, like panic mode and multi-option repairs, are either too coarse, e.g. in deleting large swathes of code, or lead to a proliferation of possible completions. This paper introduces $\texttt{tall}~\texttt{tylr}$, an error-handling parser and editor generator that completes malformed code with $\textit{syntactic obligations}$ that abstract over many possible completions. These obligations generalize the familiar notion of holes in structure editors to cover missing operands, operators, delimiters, and sort transitions. $\texttt{tall}~\texttt{tylr}$ is backed by a novel theory of tile-based parsing, conceptually organized around a $\textit{molder}$ that turns tokens into tiles and a $\textit{melder}$ that completes and parses tiles into terms using an error-handling generalization of operator-precedence parsing. We formalize melding as a parsing calculus, $\textsf{meldr}$, that completes input tiles with additional obligations such that it can be parsed into a well-formed term, with success guaranteed over all inputs. We further describe how $\texttt{tall}~\texttt{tylr}$ implements molding and completion-ranking using the principle of $\textit{minimizing obligations}$. Obligations offer a useful way to scaffold internal program representations, but in $\texttt{tall}~\texttt{tylr}$ we go further to investigate the potential of $\textit{materializing}$ these obligations visually to the programmer. We conduct a user study to evaluate the extent to which an editor like $\texttt{tall}~\texttt{tylr}$ that materializes syntactic obligations might be usable and useful, finding both points of positivity and interesting new avenues for future work.

cs.PL↗

arXiv2025

Incremental Bidirectional Typing via Order Maintenance

Live programming environments provide various semantic services, including type checking and evaluation, continuously as the user is editing the program. The live paradigm promises to improve the developer experience, but liveness is an implementation challenge particularly when working with large programs. This paper specifies and efficiently implements a system the is able to incrementally update type information for a live program in response to fine-grained program edits. This information includes type error marks and information about the expected and actual type on every expression. The system is specified type-theoretically as a small-step dynamics that propagates updates through the marked and annotated program. Most updates flow according to a base bidirectional type system. Additional pointers are maintained to connect bound variables to their binding locations, with edits traversing these pointers directly. Order maintenance data structures are employed to efficiently maintain these pointers and to prioritize the order of update propagation. We prove this system is equivalent to naive re-analysis in the Agda theorem prover, along with other important metatheoretic properties. We then implement it efficiently in OCaml, detailing a number of impactful optimizations. We evaluate this implementation's performance with a large stress-test and find that it is able to achieve dramatic speed-ups of 275.96$\times$ compared to from-scratch reanalysis.

cs.PL↗