Incremental Bidirectional Typing via Order Maintenance

This conference talk presents an incremental algorithm for maintaining total static analysis in gradually typed languages for live programming environments. Explore how the researchers from the University of Michigan and University of Utah developed a solution that efficiently updates static type information after each edit, rather than recomputing everything from scratch. Learn about the small-step dynamics used to propagate updates through an enriched program data structure, the implementation of order maintenance data structures to maintain pointers between bound variables and binding locations, and how this approach was proven equivalent to naive reanalysis using the Agda theorem prover. The presentation includes evaluation results from both real user edit traces and synthetic examples, demonstrating the algorithm's implementation in the Incremental Hazelnut language workbench. This 34-minute video was recorded at the WITS 2025 workshop on January 20, 2025, sponsored by ACM SIGPLAN.