pith. sign in

arxiv: 2510.23517 · v2 · submitted 2025-10-27 · 💻 cs.PL · cs.LO

Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors

Sidney Congard , Guillaume Munch-Maccagnoni , R\'emi Douence This is my paper

Pith reviewed 2026-05-18 03:35 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords linearityexceptionsdestructorsresource safetycall-by-push-valueCurry-Howardlinear effectsaffine types
0
0 comments X

The pith

Destructors modeled as objects in a slice category over an allocation monad integrate exceptions with linear effects while preserving resource safety.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to combine linearity, effects, and exceptions by first defining an allocation monad that tracks resource safety in a linear call-by-push-value language. Resource safety in this base calculus follows directly from the linear and ordered character of the typing rules for new and delete. Exceptions are then added by adjoining default destruction actions to types, interpreted as objects δ : A → TI in the slice category over TI. The resulting resource call-by-push-value calculus has weakening and exchange rules that perform side-effects, making the system affine at the level of types but ordered at the level of derivations. A move operation, realized as the side-effecting exchange rule, permits resource release in arbitrary order instead of strict LIFO order.

Core claim

We see destructors as objects δ : A→TI in the slice category over TI. 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.

What carries the argument

Destructors as objects δ : A → TI in the slice category over TI, adjoining default destruction actions while integrating with the allocation monad for resource safety.

If this is right

  • The linear call-by-push-value language with allocation effects new and delete is resource-safe because of its linear and ordered typing rules.
  • Exceptions integrate with the linear setting without losing resource safety once default destruction actions are adjoined via the slice category.
  • Weakening and exchange become side-effecting operations that manage resource deallocation.
  • The move operation permits resource release in random order rather than only last-in-first-out order.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same slice-category technique for adjoining actions might apply to monads modeling other effects beyond allocation.
  • The distinction between affine types and ordered derivations offers a template for designing type systems that track resources in languages supporting both linearity and exceptions.
  • One could derive explicit typing rules for a small program that allocates a resource, throws an exception, and uses a move to release it, then check whether the derivation order enforces the intended safety.

Load-bearing premise

The allocation monad T(- ⊕ E) admits the required strength in a linear setting and the slice category construction for adjoining default destruction actions preserves resource-safety properties when integrating exceptions.

What would settle it

A concrete well-typed program in the resource call-by-push-value calculus that nevertheless performs an unsafe resource access or leaves a resource unreleased after an exception is raised would show the construction fails to guarantee safety.

Figures

Figures reproduced from arXiv: 2510.23517 by Guillaume Munch-Maccagnoni, R\'emi Douence, Sidney Congard.

Figure 1
Figure 1. Figure 1: Typing rules for  Polarity annotations of expressions are inferred from the type polarities in typing rules. Hence, we will leave them implicit for typed expressions. The following notations allow to define and type expressions without restrictions with respect to values, by picking an arbitrary order to evaluate expressions. Such expressions may not always be well-typed in , since let bindings can only … view at source ↗
Figure 2
Figure 2. Figure 2: Reduction rules Indeed we can define by induction the values swap𝐴 𝑊 ∶ 𝑊 ⊗𝐴 ⟜ 𝐴⊗𝑊 (corresponding indeed to a natural isomorphism between 𝐴⊗𝑊 and 𝑊 ⊗𝐴 in the semantics of section 5): swap𝐴 𝐼 ≝ 𝜆𝑝.𝛿(𝑝, (𝑎, 𝑖).𝛿(𝑖, ().(⋆, 𝑎))) swap𝐴 𝑊1⊕𝑊2 ≝ 𝜆𝑝.𝛿(𝑝, (𝑎, 𝑤).𝛿(𝑤, 𝑤1 . let 𝑝1 = swap𝐴 𝑊1 (𝑎, 𝑤1 ) in 𝛿(𝑝1 , (𝑤1 , 𝑎).(𝜄1𝑤1 , 𝑎)), 𝑤2 . let 𝑝2 = swap𝐴 𝑊2 (𝑎, 𝑤2 ) in 𝛿(𝑝2 , (𝑤2 , 𝑎).(𝜄2𝑤2 , 𝑎)))) swap𝐴 𝑊1⊗𝑊2 ≝ 𝜆𝑝.𝛿(𝑝, … view at source ↗
Figure 3
Figure 3. Figure 3: Stack typing rules All rules that push arguments on the stack come with their dual rule that consumes the argument on the stack. Pattern match rules reduce instantly as only values can be the scrutinee. Finally, rules for constants 𝐧𝐞𝐰 and 𝐝𝐞𝐥𝐞𝐭𝐞 are the only ones that manipulate the ambient list of resources. If we interpret our previous program with the list of resources 𝑟0 ∶∶ 𝑟1 ∶∶ 𝑙, we obtain in parti… view at source ↗
Figure 4
Figure 4. Figure 4: Typing rules of ordered expressions with resources [] ⊢ 𝑆 𝑜 ⋆ ; 𝐿𝑣 ;⊢𝑜 𝑣 𝐿𝑠 ⊢ 𝑆 𝑜 𝑠 𝐿𝑠 ++ 𝐿𝑣 ⊢ 𝑆 𝑜 𝑣 · 𝑠 ; 𝐿𝑡 ; 𝑥 ⊢𝑜 𝑡 𝐿𝑠 ⊢ 𝑆 𝑜 𝑠 𝐿𝑠 ++ 𝐿𝑡 ⊢ 𝑆 𝑜 (𝑥 + .𝑡) · 𝑠 ; 𝐿𝑡 ;⊢𝑜 𝑡 𝐿𝑠 ⊢ 𝑆 𝑜 𝑠 𝐿𝑠 ++ 𝐿𝑡 ++𝑙 ⊢𝐶 𝑜 ⟨𝑡 ∣ 𝑠 ∣ 𝑙⟩ [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Typing rules of ordered stacks and commands Lemma 7. (Left SL) If ; 𝐿𝑡 ;⊢𝑜 𝑡 and Γ, 𝑥; 𝐿𝑢 ; Δ ⊢𝑜 𝑢, then Γ; 𝐿𝑡 ++ 𝐿𝑢 ; Δ ⊢𝑜 𝑢[𝑡∕𝑥]. (Right SL) If ; 𝐿𝑡 ;⊢𝑜 𝑡 and Γ; 𝐿𝑢 ; 𝑥, Δ ⊢𝑜 𝑢, then Γ; 𝐿𝑢 ++ 𝐿𝑡 ; Δ ⊢𝑜 𝑢[𝑡∕𝑥] (see ap￾pendix C.2). We then extend ⊢𝑜 for stacks and commands, with only resources in their contexts. Resources from stacks remain to the left of resources from expressions in the context of comman… view at source ↗
Figure 6
Figure 6. Figure 6: Typing rules for ,𝐦𝐨𝐯𝐞 𝑇 𝐼, which is reflected in our ordered adaptation of the interpretation of linear call-by￾push-value with a resource modality [10, Theorem 19]. The previous primitive 𝐧𝐞𝐰 ∶ 𝑅 ⊕ 1 ⟜ 1 with explicit errors is replaced by 𝐧𝐞𝐰 ∶ 𝑅 ⟜ 1: the function may throw an exception when called. Exceptions must not exchange resources during stack unwinding, so the calculus is parametrized by a def… view at source ↗
Figure 7
Figure 7. Figure 7: Predicate of linear expressions with resources C.4 Proof of (theorem 9) in the unordered case We define the indexed predicate 𝑀; Γ ⊢𝑙 𝑡 by induction with 𝑀 the multiset of resources and Γ the set of variables in 𝑡. Given a linear expression 𝑀; Γ ⊢𝑙 𝑡, we define its multiset of resources 𝑀𝑅(𝑡) ≝ 𝑀. The concatenation of contexts is always defined: Θ = (𝑀1 ; Γ1 ) @ Θ′ = (𝑀2 ; Γ2 ) ≝ 𝑀1 ,𝑀2 ; Γ1 , Γ2 . We can … view at source ↗
Figure 8
Figure 8. Figure 8: Typing rules of ordered stacks and commands ∙ 𝑣𝑤: by case analysis on the context. We then extend ⊢𝑙 for stacks and commands, with a multiset of resources and no variables: Lemma 18. Reducing a linear command results in a linear command with the same multiset of resources, i.e. for all 𝑐1 , 𝑐2 ,𝑀 such that 𝑀 ⊢𝐶 𝑙 𝑐1 and 𝑐1 ⇝ 𝑐2 one has 𝑀 ⊢𝐶 𝑙 𝑐2 . Proof. By induction on reduction steps 𝑐1 ⇝ 𝑐2: ∙ ⟨let 𝑥 + … view at source ↗
read the original abstract

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 $T(- \oplus E)$ 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 $\mathbf{new}$ and $\mathbf{delete}$. 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 $\delta : A\rightarrow TI$ in the slice category over $TI$. 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops a Curry-Howard correspondence for destructors by studying the strength of an allocation monad T(- ⊕ E) in a linear setting. It presents a linear (optionally ordered) call-by-push-value calculus with new and delete effects whose resource-safety properties are derived from the linear and ordered typing rules, then constructs a resource call-by-push-value calculus that adjoins exceptions and destructors δ : A → TI as objects in the slice category over TI. This yields a system that is affine at the level of types but ordered at the level of derivations, with weakening and exchange performing side-effects to support non-LIFO resource release.

Significance. If the constructions and preservation arguments hold, the work supplies a categorical account of resource safety under exceptions and destructors, explaining the necessity of move semantics in languages such as C++ and Rust. It strengthens the theory of linear effects by exhibiting an explicit monadic strength and a slice-category construction that integrates default destruction actions while maintaining safety.

major comments (2)
  1. [resource call-by-push-value calculus construction] The central claim that the slice-category construction adjoining δ : A → TI preserves resource-safety when weakening and exchange become side-effecting (abstract and the resource CBPV section): the manuscript must exhibit the explicit strength for the allocation monad T(- ⊕ E) in the linear category and the proof that the resulting ordered derivations remain resource-safe (no duplication or loss of resources). This is load-bearing for the integration of exceptions and destructors.
  2. [linear call-by-push-value calculus] The statement that resource-safety properties 'follow from the linear and ordered character of the typing rules' for the first calculus (abstract and linear CBPV section): the paper should provide the concrete typing rules for new and delete together with the derivation of the safety invariants, rather than leaving the argument at the level of the abstract.
minor comments (2)
  1. The notation T(- ⊕ E) and the slice category over TI would benefit from an early diagram or explicit universal property to aid readability.
  2. A short comparison paragraph with existing work on linear CBPV and effect systems (e.g., references to ordered linear logic or monadic effects) would help situate the contribution.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their detailed and constructive feedback on our manuscript. Their comments help us strengthen the exposition of the resource-safety arguments. We address each major comment below and have updated the manuscript accordingly.

read point-by-point responses

  1. Referee: [resource call-by-push-value calculus construction] The central claim that the slice-category construction adjoining δ : A → TI preserves resource-safety when weakening and exchange become side-effecting (abstract and the resource CBPV section): the manuscript must exhibit the explicit strength for the allocation monad T(- ⊕ E) in the linear category and the proof that the resulting ordered derivations remain resource-safe (no duplication or loss of resources). This is load-bearing for the integration of exceptions and destructors.

    Authors: We agree that making the strength for the allocation monad T(- ⊕ E) explicit, along with the preservation proof for resource-safety under the slice-category construction, is essential. In the revised version, we will add a dedicated subsection in the resource CBPV section that defines the monad strength in the linear category and provides a full proof that the ordered derivations (with side-effecting weakening and exchange) preserve the no-duplication and no-loss invariants for resources, even in the presence of exceptions and destructors. revision: yes

  2. Referee: [linear call-by-push-value calculus] The statement that resource-safety properties 'follow from the linear and ordered character of the typing rules' for the first calculus (abstract and linear CBPV section): the paper should provide the concrete typing rules for new and delete together with the derivation of the safety invariants, rather than leaving the argument at the level of the abstract.

    Authors: We accept this criticism. The current manuscript relies on the abstract properties without spelling out the rules. We will revise the linear CBPV section to include the full typing rules for the new and delete effects, followed by explicit inductive derivations of the safety invariants (e.g., that every allocated resource is eventually deleted exactly once, with no use after deletion). This will make the argument concrete and self-contained. revision: yes

Circularity Check

0 steps flagged

No significant circularity; resource-safety follows directly from linear/ordered typing rules and slice-category construction

full rationale

The paper introduces the allocation monad T(- ⊕ E) to model resource safety and defines two calculi whose safety properties are stated to follow from the linear and ordered character of the typing rules (first calculus) and from the slice-category construction adjoining destructors δ : A → TI (second calculus). These are presented as direct consequences of the definitions and standard categorical notions rather than fitted parameters or self-referential reductions. No equations or steps are shown to equate a claimed prediction back to its own inputs by construction, and the abstract does not rely on load-bearing self-citations for the core claims. The derivation remains self-contained against the stated assumptions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claims rest on standard assumptions from linear logic and category theory together with newly introduced modeling constructs for the allocation monad and destructors; no independent evidence for the new entities is provided beyond the abstract description.

axioms (1)
  • standard math Standard monad laws and linear logic properties hold for the allocation monad T(- ⊕ E)
    Invoked to model effects and ensure resource-safety in the linear setting.
invented entities (2)
  • Allocation monad T(- ⊕ E) no independent evidence
    purpose: To model and study resource-safety properties for allocation effects new and delete
    Introduced specifically for the first calculus to capture allocation in a linear setting.
  • Destructors δ : A → TI as objects in the slice category over TI no independent evidence
    purpose: To adjoin default destruction actions to types for handling exceptions while preserving linearity
    Formalized to integrate exceptions with effects and resource safety, inspired by C++/Rust.

pith-pipeline@v0.9.0 · 5784 in / 1445 out tokens · 60788 ms · 2026-05-18T03:35:03.925376+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

58 extracted references · 58 canonical work pages · 1 internal anchor

  1. [1]

    Use-Once

    Baker, H.G.: “Use-Once” Variables and Linear Objects - Storage Management, Reflection and Multi-Threading. SIGPLAN Notices30(1), 45–52 (1995).https://doi.org/10.1145/ 199818.199860

    work page arXiv 1995

  2. [2]

    Baker,H.G.:Linearlogicandpermutationstacks-theForthshallbefirst.SIGARCHComputer Architecture News22(1), 34–43 (1994).https://doi.org/10.1145/181993.181999

    work page doi:10.1145/181993.181999 1994

  3. [3]

    Look ma, no garbage!

    Baker, H.G.: Lively linear lisp: “Look ma, no garbage!” ACM Sigplan notices27(8), 89–98 (1992)

    work page 1992

  4. [4]

    https://doi.org/10.1017/S0956796801004099

    Benton,N.,Kennedy,A.:Exceptionalsyntax.JournalofFunctionalProgramming 11,395–410 (2001). https://doi.org/10.1017/S0956796801004099

    work page doi:10.1017/s0956796801004099 2001

  5. [5]

    In: Proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW’01), pp

    Berdine, J., O’Hearn, P.W., Reddy, U.S., Thielecke, H.: Linearly used continuations. In: Proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW’01), pp. 47–54 (2000)

    work page 2000

  6. [6]

    PACMPL2(POPL), 5:1–5:29 (2018)

    Bernardy, J., Boespflug, M., Newton, R.R., Peyton Jones, S., Spiwack, A.: Linear Haskell: practical linearity in a higher-order polymorphic language. PACMPL2(POPL), 5:1–5:29 (2018). https://doi.org/10.1145/3158093

    work page doi:10.1145/3158093 2018

  7. [7]

    Mathematical Structures in Computer Science6(4), 313–351 (1996)

    Blute, R., Cockett, J., Seely, R.: ! and ?-Storage as tensorial strength. Mathematical Structures in Computer Science6(4), 313–351 (1996)

    work page 1996

  8. [8]

    In: International Colloquium on Automata, Languages, and Programming, pp

    Braüner, T.: A model of intuitionistic affine logic from stable domain theory. In: International Colloquium on Automata, Languages, and Programming, pp. 340–351 (1994)

    work page 1994

  9. [9]

    In: LOLA 2018: Workshop on Syntax and Semantics of Low-Level Languages (2018).https://hal

    Combette, G., Munch-Maccagnoni, G.: A resource modality for RAII (abstract). In: LOLA 2018: Workshop on Syntax and Semantics of Low-Level Languages (2018).https://hal. inria.fr/hal-01806634

    work page 2018

  10. [10]

    In: Proc

    Curien, P.-L., Fiore, M., Munch-Maccagnoni, G.: A Theory of Effects and Resources: Adjunc- tion Models and Polarised Calculi. In: Proc. POPL (2016).https://doi.org/10.1145/ 2837614.2837652

    work page arXiv 2016

  11. [11]

    In: MacLane, S., Applegate, H., Barr, M., Day, B., Dubuc,E., Phreilambud,Pultr, A.,Street, R.,Tierney,M., Swierczkowski,S

    Day, B.: On closed categories of functors. In: MacLane, S., Applegate, H., Barr, M., Day, B., Dubuc,E., Phreilambud,Pultr, A.,Street, R.,Tierney,M., Swierczkowski,S. (eds.)Reports of the Midwest Category Seminar IV, pp. 1–38. Springer Berlin Heidelberg, Berlin, Heidelberg (1970)

    work page 1970

  12. [12]

    -H.,Marché,C.:Creusot:aFoundryfortheDeductiveVerificationofRust Programs

    Denis,X.,Jourdan,J. -H.,Marché,C.:Creusot:aFoundryfortheDeductiveVerificationofRust Programs. In: ICFEM 2022 - 23th International Conference on Formal Engineering Methods. LNCS, Springer, Heidelberg (2022).https://inria.hal.science/hal-03737878

    work page 2022

  13. [13]

    In: Proc

    Filinski, A.: Linear Continuations. In: Proc. POPL, pp. 27–38 (1992)

    work page 1992

  14. [14]

    In: Proc

    Filinski, A.: Representing Monads. In: Proc. POPL, pp. 446–457. ACM Press (1994)

    work page 1994

  15. [15]

    In: Sestoft, P

    Fluet, M., Morrisett, G., Ahmed, A.J.: Linear Regions Are All You Need. In: Sestoft, P. (ed.) Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings. LNCS, vol. 3924, pp. 7–21. Spring...

    work page doi:10.1007/11693024_2 2006

  16. [16]

    In: Alves, S., Cervesato, I

    Gan, E., Tov, J.A., Morrisett, G.: Type Classes for Lightweight Substructural Types. In: Alves, S., Cervesato, I. (eds.) Proceedings Third International Workshop on Linearity, LINEARITY 2014, Vienna, Austria, 13th July, 2014. EPTCS, pp. 34–48 (2014).https://doi.org/10. 4204/EPTCS.176.4

    work page 2014

  17. [17]

    Theoretical Computer Science50, 1–102 (1987)

    Girard, J.-Y.: Linear Logic. Theoretical Computer Science50, 1–102 (1987)

    work page 1987

  18. [18]

    In: Knoop, J., Hendren, L.J

    Grossman, D., Morrisett, J.G., Jim, T., Hicks, M.W., Wang, Y., Cheney, J.: Region-Based Memory Management in Cyclone. In: Knoop, J., Hendren, L.J. (eds.) Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002, pp. 282–293. ACM (2002).https://doi.org/10. 1145/512529.512563

    work page arXiv 2002

  19. [19]

    Linear Exponential Comonads without Symmetry

    Hasegawa, M.: Linear Exponential Comonads without Symmetry. In: Fourth International Workshop on Linearity (2016).http://arxiv.org/abs/1701.04919

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  20. [20]

    In: Hu, Z., Rodríguez-Artalejo, M

    Hasegawa, M.: Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus. In: Hu, Z., Rodríguez-Artalejo, M. (eds.) Functional and Logic Program- ming, 6th International Symposium, FLOPS 2002, Aizu, Japan, September 15-17, 2002, Proceedings. LNCS, vol. 2441, pp. 167–182. Springer, Heidelberg (2002).https://doi. org/10.1007/3-54...

    work page doi:10.1007/3-540-45788-7_10 2002

  21. [21]

    In: International Symposium on Functional and Logic Programming, pp

    Hasegawa, M.: Semantics of linear continuation-passing in call-by-name. In: International Symposium on Functional and Logic Programming, pp. 229–243 (2004)

    work page 2004

  22. [22]

    Hinnant, H.E., Dimov, P., Abrahams, D.: A Proposal to Add Move Semantics Support to the C++ Language, (2002).http://www.open-std.org/jtc1/sc22/wg21/docs/papers/ 2002/n1377.htm

    work page 2002

  23. [23]

    Lang.6(ICFP) (2022).https://doi.org/10.1145/3547647

    Ho,S.,Protzenko,J.:Aeneas:RustVerificationbyFunctionalTranslation.Proc.ACMProgram. Lang.6(ICFP) (2022).https://doi.org/10.1145/3547647

    work page doi:10.1145/3547647 2022

  24. [24]

    Hofmann, M.: A Type System for Bounded Space and Functional In-Place Update. Nord. J. Comput.7(4), 258–289 (2000)

    work page 2000

  25. [25]

    PACMPL2(POPL), 66:1–66:34 (2018).https://doi.org/10

    Jung, R., Jourdan, J., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the rust programming language. PACMPL2(POPL), 66:1–66:34 (2018).https://doi.org/10. 1145/3158154

    work page 2018

  26. [26]

    In: Proceedings of the C++ Confer- ence

    Koenig, A., Stroustrup, B.: Exception Handling for C++. In: Proceedings of the C++ Confer- ence. San Francisco, CA, USA, April 1990, pp. 149–176 (1990)

    work page 1990

  27. [27]

    Lafont,Y.:Thelinearabstractmachine.Theoreticalcomputerscience 59(1-2),157–180(1988)

    work page 1988

  28. [28]

    Levy, P.B.: Call-By-Push-Value: A Functional/Imperative Synthesis (Semantics Structures in Computation, V. 2). Kluwer Academic Publishers, USA (2004)

    work page 2004

  29. [29]

    In: Proc

    Levy, P.B.: Call-by-Push-Value: A Subsuming Paradigm. In: Proc. TLCA ’99, pp. 228–242 (1999)

    work page 1999

  30. [30]

    400–414 (2017)

    Levy,P.B.:Contextualisomorphisms.In:Proceedingsofthe44thACMSIGPLANSymposium on Principles of Programming Languages, pp. 400–414 (2017)

    work page 2017

  31. [31]

    In: Proc

    Maraist,J.,Odersky,M.,Turner,D.N.,Wadler,P.:Call-by-Name,Call-by-Value,Call-by-Need, and the Linear Lambda Calculus. In: Proc. MFPS ’95 (1994)

    work page 1994

  32. [32]

    Categorical models of linear logic revisited

    Melliès, P.-A.: “Categorical models of linear logic revisited”. working paper or preprint

    work page

  33. [33]

    Categorical semantics of linear logic

    Melliès, P.-A.: “Categorical semantics of linear logic”. In: vol. 27. Panoramas et Synthèses. Société Mathématique de France, 2009. Chap. 1, pp. 15–215

    work page 2009

  34. [34]

    Parametric monads and enriched adjunctions

    Melliès, P.-A.: “Parametric monads and enriched adjunctions”. Draft

    work page

  35. [35]

    Møgelberg, R.E., Staton, S.: Linear usage of state. Log. Methods Comput. Sci.10(1) (2014). https://doi.org/10.2168/LMCS-10(1:17)2014

    work page doi:10.2168/lmcs-10(1:17)2014 2014

  36. [36]

    Moggi,E.:Computationallambda-calculusandmonads.In:ProceedingsoftheFourthAnnual IEEE Symposium on Logic in Computer Science (LICS 1989), pp. 14–23. IEEE Computer Society Press, Pacific Grove, CA, USA (1989)

    work page 1989

  37. [37]

    Information and Computation93(1), 55– 92 (1991)

    Moggi, E.: Notions of computation and monads. Information and Computation93(1), 55– 92 (1991). https : / / doi . org / 10 . 1016 / 0890 - 5401(91 ) 90052 - 4. https : / / www . sciencedirect.com/science/article/pii/0890540191900524

    work page arXiv 1991

  38. [38]

    Logical Methods in Computer Science, Volume 14, Issue 4 (November 15, 2018) lmcs:4973 (2018).https://doi.org/10.23638/ LMCS-14(4:14)2018

    Mostrous, D., Vasconcelos, V.T.: Affine Sessions. Logical Methods in Computer Science, Volume 14, Issue 4 (November 15, 2018) lmcs:4973 (2018).https://doi.org/10.23638/ LMCS-14(4:14)2018. arXiv:1809.02781v2 [cs.LO]

    work page arXiv 2018

  39. [39]

    Resource Polymorphism

    Munch-Maccagnoni, G.: “Resource Polymorphism”

    work page

  40. [40]

    Orchard, D., Liepelt, V.-B., Eades III, H.: Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang.3(ICFP) (2019).https://doi.org/10.1145/3341714

    work page doi:10.1145/3341714 2019

  41. [41]

    SPLASH’16,pp.234–251.ACM(2016).https://doi.org/10.1145/2983990.2984009

    Osvald,L.,Essertel,G.,Wu,X.,Alayón,L.I.G.,Rompf,T.:Gentrificationgonetoofar?afford- able2nd-classvaluesforfunand(co-)effect.In:Proceedingsofthe2016ACMSIGPLANInter- nationalConferenceonObject-OrientedProgramming,Systems,Languages,andApplications. SPLASH’16,pp.234–251.ACM(2016).https://doi.org/10.1145/2983990.2984009

    work page doi:10.1145/2983990.2984009 2016

  42. [42]

    In: Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS2009,11-14August2009,LosAngeles,CA,USA,pp.101–110.IEEEComputerSociety (2009)

    Pfenning, F., Simmons, R.J.: Substructural Operational Semantics as Ordered Logic Program- ming. In: Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS2009,11-14August2009,LosAngeles,CA,USA,pp.101–110.IEEEComputerSociety (2009). https://doi.org/10.1109/LICS.2009.8

    work page doi:10.1109/lics.2009.8 2009

  43. [43]

    Notions of Computation Determine Monads

    Plotkin, G., Power, J.: “Notions of Computation Determine Monads”. In: Foundations of SoftwareScienceandComputationStructures.SpringerBerlinHeidelberg,2002,pp.342–356. ISBN: 9783540459316.https://doi.org/10.1007/3-540-45931-6_24

    work page doi:10.1007/3-540-45931-6_24 2002

  44. [44]

    PhD thesis, Carnegie Mellon University (2001)

    Polakow, J.: Ordered Linear Logic and Applications. PhD thesis, Carnegie Mellon University (2001)

    work page 2001

  45. [45]

    In: Kuchen, H., Ueda, K

    Polakow, J., Yi, K.: Proving Syntactic Properties of Exceptions in an Ordered Logical Frame- work. In: Kuchen, H., Ueda, K. (eds.) Functional and Logic Programming, 5th International Symposium, FLOPS 2001, Tokyo, Japan, March 7-9, 2001, Proceedings. LNCS, vol. 2024, pp. 61–77. Springer, Heidelberg (2001).https://doi.org/10.1007/3-540-44716-4_4

    work page doi:10.1007/3-540-44716-4_4 2001

  46. [46]

    Mathematical Structures in Computer Science5(7), 453–468 (1997)

    Power, A.J., Robinson, E.: Premonoidal categories and notions of computation. Mathematical Structures in Computer Science5(7), 453–468 (1997)

    work page 1997

  47. [47]

    https://doi.org/10.1016/S0304-3975(00)00340-6

    Power,J.:Premonoidalcategoriesascategorieswithalgebraicstructure.TheoreticalComputer Science278(1),303–321(2002). https://doi.org/10.1016/S0304-3975(00)00340-6. https://www.sciencedirect.com/science/article/pii/S0304397500003406

    work page doi:10.1016/s0304-3975(00)00340-6 2002

  48. [48]

    Lecture Notes in Computer Science4962, 81–96 (2008)

    Selinger, P., Valiron, B.: A linear-non-linear model for a computational call-by-value lambda calculus. Lecture Notes in Computer Science4962, 81–96 (2008)

    work page 2008

  49. [49]

    In: The Second ACM SIGPLAN Conference on History of Programming Languages

    Stroustrup, B.: A History of C++: 1979–1991. In: The Second ACM SIGPLAN Conference on History of Programming Languages. HOPL-II, pp. 271–297. Association for Computing Machinery,Cambridge,Massachusetts,USA(1993). https://doi.org/10.1145/154766. 155375

    work page doi:10.1145/154766 1979

  50. [50]

    Science of Computer Programming62(2), 122–144 (2006)

    Swamy,N.,Hicks,M.,Morrisett,G.,Grossman,D.,Jim,T.:Safemanualmemorymanagement in Cyclone. Science of Computer Programming62(2), 122–144 (2006)

    work page 2006

  51. [51]

    Information and computation 132(2), 109–176 (1997)

    Tofte, M., Talpin, J.-P.: Region-based memory management. Information and computation 132(2), 109–176 (1997)

    work page 1997

  52. [52]

    PhD thesis, Northeastern Univer- sity (2012)

    Tov, J.A.: Practical Programming with Substructural Types. PhD thesis, Northeastern Univer- sity (2012)

    work page 2012

  53. [53]

    In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications

    Tov, J.A., Pucella, R.: A Theory of Substructural Types and Control. In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications. OOPSLA ’11, pp. 625–642. ACM, Portland, Oregon, USA (2011).https: //doi.org/10.1145/2048066.2048115 . http://doi.acm.org/10.1145/2048066. 2048115

    work page doi:10.1145/2048066.2048115 2011

  54. [54]

    In: Ball, T., Sagiv, M

    Tov, J.A., Pucella, R.: Practical affine types. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pp. 447–458. ACM (2011).https: //doi.org/10.1145/1926385.1926436

    work page doi:10.1145/1926385.1926436 2011

  55. [55]

    record . txt

    Walker, D.: Substructural type systems. In: Advanced Topics in Types and Programming Languages. Ed. by B.C. Pierce, pp. 3–44. The MIT Press (2005) A Context: resource management in programming Programmers must sometimes deal withresources: values denoting some memory al- locations, files, locks, etc.—in general reifying some knowledge about the state of t...

    work page 2005

  56. [56]

    disposing of the resource in a timely fashion in all the code paths (avoiding leaks, as we have seen),

    work page

  57. [57]

    keepingtrackofwhoisresponsiblefordisposingoftheresource(toavoidforinstance that the resource is disposed of twice),

    work page

  58. [58]

    record . txt

    making sure that a resource is never used after its disposal (use-after-free). In simple situations like the previous one, and in languages that support it, the resources can be managed automatically with higher-order scoped combinators derived from LISP’sunwind-protect: wi th _f il e (" record . txt " , 𝜆 f . append (f , " starting tasks "); wi th _f il ...

    work page 1980