2025-winter

Speaker	Time ∧ Location	Paper
	Abstract
Russell Rozenbaum	April 4th, 4-5pm in 4901 BBB	Structure-Level Interactions in LLM-Based Coding Agents
	This work explores the development of structure-based action languages for LLM-powered coding agents, moving beyond traditional line-based approaches. We hypothesize that line-based interactions undermine the semantical abstractions naturally used when coding. Our research integrates LLM agents with Hazel, a live functional programming environment capable of structure-level editing and semantic analysis even in incomplete programs. By equipping agents with higher-level, structure-based actions, we aim to enhance their code generation capabilities. Additionally, we develop an interactive user interface for human-agent collaboration. This research contributes to both automated program synthesis and programming education, while addressing the semantic contextualization challenges faced by existing LLM-based coding assistants.
Matthew Keenan	February 14th, 4-5pm in 4901 BBB	Explicit Refinement Types
	We present 𝜆ert, a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs of properties within the program text, letting us support a rich logic of properties including quantifiers and induction. We show that the type system is sound by showing that every refined program erases to a simply-typed program, and by means of a denotational semantics, we show that every erased program has all of the properties demanded by its refined type. All of our proofs are formalised in Lean 4.
Thomas J. Porter	January 17th, 4-5pm in 2901 BBB	Incremental Bidirectional Typing via Order Maintenance
	In live programming systems, editor services such as type checking and evaluation are continually provided while the user is editing the program. The live paradigm offers benefits to developer experience and productivity. Generally editor services are stateless transformations that take only the current the program text as input, and compute the result from scratch. This presents a challenge to implementing live editors at scale, since the execution time will grow with the size of the program, and at some point will take too long to be recomputed between each edit. This work presents a solution in the form of an incremental algorithm for maintaining a total static analysis of a program in a simple gradually typed language. Each edit action triggers an update to an enriched program data structure, yielding updated static information more efficiently than a fresh pass would. The algorithm is presented as a small-step dynamics to propagate updates through the enriched program data structure. Most updates flow according to the base bidirectional type system. Additional pointers are maintained to connect bound variables and their binding locations. Order maintenance data structures are employed to efficiently maintain these pointers and to prioritize the order of update propagation. We prove this algorithm equivalent to naive reanalysis in the Agda theorem prover. We implement the algorithm in the Incremental Hazelnut language workbench. We evaluate its performance on edit traces from real users as well as synthetic examples.