HATRA 2023
who it's for
programming language researchers, language tool developers, compiler engineers, ide and editor plugin developers, type system designers, verification and theorem proving researchers, rust developers, programming education researchers
topics
grid and box diagram templates for provers; multi-wizard program synthesis study; lightweight aliasing for Java (shared/unique/owned); destructive reads without runtime changes; trait solver proof trees and visualization; live programming with holes (Hazel); Agda proof of edit-preservation; Rust lifetime SVG diagnostics; semantic subtyping in Luau; infallible type assignment and error suppression
| title | author | length |
|---|---|---|
| Diagrammatic notations for interactive theorem proving | Shardul Chiplunkar, Clément Pit-Claudel | 29m |
Argues that interactive theorem provers need declarative diagram languages that match text macros by delivering low-cost composition and good-looking idioms… | ||
| Exploratory Study on Multi-User Program Synthesis: A Multi-Wizard Approach | Tyler Holloway, Nada Amin, Elena L. Glassman | 25m |
Proposes two study designs: a between-subjects lab with 24 participants (pairs vs individuals, each doing one task with and one without a synthesizer) and a… | ||
| Latte: Lightweight Aliasing Tracking for Java | Conrad Zimmerman, Catarina Gamboa, Alcides Fonseca, Jonathan Aldrich | 33m |
Latte adds a lightweight aliasing layer to Java that only requires annotations on parameters and fields while inferring local variable annotations, tracks… | ||
| Debugging Trait Errors as Logic Programs | Gavin Gray, Will Crichton | 30m |
Rust trait resolution is literally a Prolog‑style logic program and compiler diagnostics collapse once constraints grow — real Bevy docs show 92 trait impls… | ||
| Totally Live Programming with Hazel (Progress Report) | Cyrus Omar, Andrew Blinn, David Moon | 32m |
Hazel is a structure editor that keeps every editor state syntactically and statically meaningful by inserting hexagonal holes for missing pieces and by… | ||
| REVIS: An Error Visualization Tool for Rust | Ruochen Wang, Molly MacLaren, Michael Coblenz | 29m |
A VSCode extension visualizes lifetime-related Rust compiler errors as SVG line decorations showing regions for lifetimes, arrows for moves/borrows, and… | ||
| Goals of the Luau Type System, Two Years On | Lily Brown, Andy Friesen, Alan Jeffrey | 35m |
Roblox reports it implements semantic subtyping by normalizing types (with possible exponential blowup) to reduce false positives, and it builds an infallible… | ||
| nothing matches | ||