Tootfinder

Destination calculus: A linear λ-calculus for purely functional memory writes
Presented by Arnaud Spiwack. Joint work with Thomas Bagrel,
#icfpsplash25

Substitution Without Copy and Paste
Thorsten Altenkirch (University of Nottingham), Nathaniel Burke (Imperial College London), Philip Wadler (University of Edinburgh)
https://arxiv.org/abs/2510.12304

Substitution Without Copy and Paste
Defining substitution for a language with binders like the simply typed $λ$-calculus requires repetition, defining substitution and renaming separately. To verify the categorical properties of this calculus, we must repeat the same argument many times. We present a lightweight method that avoids repetition and that gives rise to a simply typed category with families (CwF) isomorphic to the initial simply typed CwF. Our paper is a literate Agda script.