Reference. Adjoint Natural Deduction
Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.
Cite
Cited by (2)
Ordered Adjoint Logic roshal-2026-ordered
Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most formulations, ordered types are also linear, requiring each resource to be used exactly once. Prior work by Kanovich et al. has investigated calculi that relax this constraint through subexponentials within a linear ordered logic. We generalize their work by using adjoint modalities to combine logics with varying fine-grained structural properties, including weakening, left contraction, right contraction, left mobility, and right mobility. We show that the resulting sequent calculus admits cut elimination. We further provide a natural deduction formulation in which structural rules are implicit, and show that proof checking for this system is decidable. This makes it a suitable foundation for an expressive adjoint programming language or logical framework.
Substructural Parametricity aberle-2025-substructural
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.
Cites 51 works (4 here)
With notes (4)
Relating Message Passing and Shared Memory, Proof-Theoretically pfenning-2023-relating
A Framework for Substructural Type Systems wood-2022-a
Mechanisation of programming language research is of growing interest, and the act of mechanising type systems and their metatheory is generally becoming easier as new techniques are invented. However, state-of-the-art techniques mostly rely on structurality of the type system — that weakening, contraction, and exchange are admissible and variables can be used unrestrictedly once assumed. Linear logic, and many related subsequent systems, provide motivations for breaking some of these assumptions. We present a framework for mechanising the metatheory of certain substructural type systems, in a style resembling mechanised metatheory of structural type systems. The framework covers a wide range of simply typed syntaxes with semiring usage annotations, via a metasyntax of typing rules. The metasyntax for the premises of a typing rule is related to bunched logic, featuring both sharing and separating conjunction, roughly corresponding to the additive and multiplicative features of linear logic. We use the uniformity of syntaxes to derive type system-generic renaming, substitution, and a form of linearity checking.
Syntax and Semantics of Quantitative Type Theory atkey-2018-syntax
Session Types as Intuitionistic Linear Propositions caires-2010-session
External (47)
- Adjoint Logic with Applications (2024)
- The Rust programming language (2024)
- A graded modal dependent type theory with a universe and erasure, formalized (2023)
- Combining dependency, grades, and adjoint logic (2023)
- Back to futures (2022)
- A graded dependent type system with a usage-aware semantics (2021)
- Graded modal dependent type theory (2021)
- A message-passing interpretation of adjoint logic (2021)
- Resourceful program synthesis from graded linear types (2020)
- A logical framework with commutative and non-commutative subexponentials (2018)
- Subexponentials in non-commutative linear logic (2017)
- A fibrational framework for substructural and modal logics (2017)
- Linear logic propositions as session types (2016)
- Practical Foundations for Programming Languages (2016)
- Adjoint logic with a 2-category of modes (2016)
- An extended framework for specifying and reasoning about proof systems (2016)
- Distilling abstract machines (2014)
- Propositions as sessions (2012)
- Practical affine types (2011)
- Classical and intuitionistic subexponential logics are equally expressive (2010)
- Algorithmic specifications in linear logic with subexponentials (2009)
- A judgmental deconstruction of modal logic (2009)
- Contextual modal type theory (2008)
- Call-by-push-value: Decomposing call-by-value and call-by-name (2006)
- A judgmental analysis of linear logic (2003)
- Efficient resource management for linear logic proof search (2000)
- A judgmental reconstruction of modal logic (1999)
- Computational types from a logical perspective (1998)
- Dual intuitionistic linear logic (1996)
- Linear logic, monads, and the lambda calculus (1996)
- Natural deduction for intuitionistic linear logic (1995)
- A mixed linear and non-linear logic: Proofs, terms and models (1994)
- A mixed linear and non-linear logic: Proofs, terms and models (preliminary report) (1994)
- Computational interpretations of linear logic (1993)
- Subtyping recursive types (1993)
- A term calculus for intuitionistic linear logic (1993)
- A natural semantics for lazy evaluation (1993)
- Logic programming with focusing proofs in linear logic (1992)
- Linear types can change the world (1990)
- Linear logic and lazy computation (1987)
- On the meanings of the logical constants and the justifications of the logical laws (1983)
- The theory and practice of transforming call-by-need into call-by-value (1980)
- The Logical Basis of Metaphysics (1976)
- Untersuchungen über das logische Schließen (1969)
- The formulae-as-types notion of construction (1969)
- Introduction to Metamathematics (1952)
- The Calculi of Lambda-Conversion (1941)