Ordered Adjoint Logic (Extended Version)

TL;DR

This paper introduces a generalized ordered adjoint logic using adjoint modalities, enabling flexible structural properties and providing a decidable proof system suitable for programming languages and frameworks.

Contribution

It extends prior ordered logic work by incorporating adjoint modalities to combine various structural rules, ensuring cut elimination and decidability in proof checking.

Findings

The sequent calculus admits cut elimination.

Proof checking is decidable.

The logic supports a range of structural properties through adjoint modalities.

Abstract

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.