Klaas Pruiksma

Adjoint Logic with Applications Degree Type: Ph.D. in Computer Science
Advisor(s): Frank Pfenning
Graduated: May 2024

Abstract:

Many different systems of logic, such as linear logic, lax logic, and various modal logics have been studied extensively and find applications in diverse domains. Likewise, in the context of programming languages, many different language features have been explored fruitfully. In both cases, however, these different features are often studied in isolation, or in the context of some simple base language. As such, it can be unclear how these features interact, if we want to work with a programming language combining different features, or a logic that allows us to model behavior from several different base logics.

Adjoint logic is a framework or schema for defining logics based on a set of modes, each of which represents a single base logic. These base logics are thencombined uniformly and coherently into a single instance of adjoint logic. In this document, we will develop a form of adjoint logic that forms a suitable basis for concurrent programming languages. We first develop the proof theory of adjoint logic, proving generically useful logical results such as cut elimination, identity expansion, and focusing. This ensures that our approach to adjoint logic yields a sensible proof system, and means that we can get these results for free for a given logic by showing that it is an instance of adjoint logic.

Interpreting proof reduction as communication between concurrent processes, particularly using a semi-axiomatic sequent calculus formulation to model asynchronous communication, we can convert the framework of adjoint logic into a similar adjoint framework for programming languages. By making use of different modes, we can model a range of communication behavior, notably including multicast, where a message is sent to multiple recipients. We also see that with a different interpretation, we can model communication via shared memory, which then also lends itself well to reconstructing sequential computation within this concurrent language. Additionally, the uniformity of this framework means that as we add features to (or encode features into) these languages, we will naturally also be able to work with multi-featural languages, perhaps restricted by mode.

Further building on these languages, we then explore notions of program equivalence in the adjoint setting, which may be useful both for the development of dependent adjoint types, as well as for reasoning about programs, particularly in the context of optimization. A first handling of a uniformly defined equivalence across all modes provides a blueprint for how to work with equivalence in the adjoint setting, particularly handling situations where some, but not all data may be reused, and addressing the intuitive idea of equivalence when communication is limited to a specific interface, which may consist of multiple channels/memory addresses, each with their own specification for communication behavior. Using this, we can then examine several examples of mode-dependent equivalence, where we combine multiple different notions of equivalence coherently into one.

Thesis Committee:
Frank Pfenning (Chair)
Stephanie Balzer
Henry DeYoung
Robert Harper
Andrew Pitts (University of Cambridge, Emeritus)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Keywords:
Proof Theory, Programming Languages, Adjoint Logic, Program Equivalence