Person. Sidney Congard

Papers

Linear Effects, Exceptions, and Resource Safety: A Curry-Howard Correspondence for Destructors congard-2026-linear

We analyse the problem of combining linearity, effects, and exceptions, in abstract models of programming languages, as the issue of providing some kind of strength for a monad 𝑇(βˆ’βŠ•πΈ) in a linear setting. We consider in particular for T the allocation monad, which we introduce to model and study resource-safety properties. We apply these results to a series of two linear effectful calculi for which we establish their resource-safety properties. The first calculus is a linear (optionally ordered) call-by-push-value language with two allocation effects 𝐧𝐞𝐰 and 𝐝𝐞π₯𝐞𝐭𝐞. The resource-safety properties follow from the linear and ordered character of the typing rules. We then integrate exceptions with linearity and effects by adjoining default destruction actions to types, as inspired by C++/Rust destructors. We see destructors as objects 𝛿:𝐴→𝑇𝐼 in the slice category over 𝑇𝐼. This construction gives rise to a second calculus, the resource call-by-push-value, featuring exceptions and destructors, and whose weakening and exchange rules perform side-effects. It is therefore affine at the level of types but ordered at the level of derivations. As in C++ and Rust, a β€œmove” operationβ€”the side-effecting exchange ruleβ€”is necessary for releasing resources in random order, as opposed to LIFO order.
PDF Β· DOI Β· arXiv Β· pldb
sidneycongard person entries/rolodex/sidneycongard.hel