Showing cs.PLShow all
3 papers · 1 filter
cs.PL2026
Potential Functions as Types
Harrison Grodin, Ethan Chu, Runming Li +2
Amortized analysis can be framed from the physicist's view, amenable to manual verification in dependent type theory using potential functions, and the banker's view, amenable to a…
cs.PL2025
Efficient Cost Bounds with Linear Maps
David M Kahn, Jan Hoffmann, Thomas Reps +1
The Automatic Amortized Resource Analysis (AARA) derives program-execution cost bounds using types. To do so, AARA often makes use of cost-free types, which are critical for the co…
cs.PL2025
Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
David M Kahn, Jan Hoffmann, Runming Li
As is evident in the programming language literature, many practitioners favor specifying dynamic program behavior using big-step over small-step semantics. Unlike small-step seman…