Cover Image

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

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Congard, Sidney, Munch-Maccagnoni, Guillaume, Douence, Rémi
Format:	Preprint
Published:	2025
Subjects:	Programming Languages Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

S4 modal sequent calculus as intermediate logic and intermediate language
by: Caspar, Jean, et al.
Published: (2026)

Classical notions of computation and the Hasegawa-Thielecke theorem (extended version)
by: Mangel, Éléonore, et al.
Published: (2025)

A Curry-Howard Correspondence for Linear, Reversible Computation
by: Chardonnet, Kostia, et al.
Published: (2023)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
by: Castagna, Giuseppe, et al.
Published: (2024)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Linearization via Rewriting (Long Version)
by: Lago, Ugo Dal, et al.
Published: (2025)

Termination Analysis of Linear-Constraint Programs
by: Ben-Amram, Amir M., et al.
Published: (2025)

Linear Contextual Metaprogramming and Session Types
by: Ângelo, Pedro, et al.
Published: (2024)

JAX Autodiff from a Linear Logic Perspective (Extended Version)
by: Giusti, Giulia, et al.
Published: (2025)

Dependent Multiplicities in Dependent Linear Type Theory
by: Doré, Maximilian
Published: (2025)

Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
by: Accattoli, Beniamino
Published: (2022)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
by: Vollmer, Victoria, et al.
Published: (2024)

Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability
by: Akshay, S., et al.
Published: (2026)

On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System
by: Matsuoka, Satoshi
Published: (2026)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
by: Rustenholz, Louis, et al.
Published: (2024)

Towards a Certified Proof Checker for Deep Neural Network Verification
by: Desmartin, Remi, et al.
Published: (2023)

Frex: dependently-typed algebraic simplification
by: Allais, Guillaume, et al.
Published: (2023)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
by: Desmartin, Remi, et al.
Published: (2024)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

Syntax and Semantics of Linear Dependent Types
by: Vákár, Matthijs
Published: (2014)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
by: Viennot, Jules, et al.
Published: (2025)

Exploiting the Potential of Linearity in Automatic Differentiation and Computational Cryptography
by: Giusti, Giulia
Published: (2025)

Meaningfulness and Genericity in a Subsuming Framework
by: Kesner, Delia, et al.
Published: (2024)

RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
by: Matsushita, Yusuke, et al.
Published: (2025)

Towards a Higher-Order Bialgebraic Denotational Semantics
by: Goncharov, Sergey, et al.
Published: (2026)

A uniform characterisation of the (a)synchronous must-preorder
by: Bernardi, Giovanni, et al.
Published: (2026)

From Time to Space: The Impact of Linearity in Higher-Order Datalog
by: Charalambidis, Angelos, et al.
Published: (2026)

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics
by: Soldevila, Mallku, et al.
Published: (2024)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
by: Elad, Neta, et al.
Published: (2023)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
by: Verscht, Lena, et al.
Published: (2024)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

A Probabilistic Choreography Language for PRISM
by: Carbone, Marco, et al.
Published: (2025)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

Positive Sharing and Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

Expressive Power of One-Shot Control Operators and Coroutines
by: Kobayashi, Kentaro, et al.
Published: (2025)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
by: Elad, Neta, et al.
Published: (2025)

The Functional Machine Calculus III: Control
by: Heijltjes, Willem
Published: (2025)

Orthologic Type Systems
by: Guilloud, Simon, et al.
Published: (2025)