Computer Science Thesis Oral
— 11:30am
Location:
In Person and Virtual - ET
-
Traffic21 Classroom, Gates Hillman 6501 and Zoom
Speaker:
KLAAS PRUIKSMA
,
Ph.D. Candidate, Computer Science Department, Carnegie Mellon University
Adjoint Logic with Applications
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 then combined uniformly and coherently into a single instance of adjoint logic.
In this talk, we will present a form of adjoint logic that is a suitable basis for concurrent/parallel programming languages. We will first develop the proof theory of adjoint logic, establishing generally useful logical results such as cut elimination and focusing. By interpreting the proof reductions found in cut elimination as communication steps between processes running in parallel, we can convert the framework of adjoing logic into a similarly broad framework for programming languages, which model a range of communication behaviour, notably including multicast, where a single message is sent to multiple recipients. Recasting our interpretation of this language, we are also able to model communication via futures, a limited form of write-once shared memory, and this interpretation also enables us to reconstruct sequential computation, despite the natural parallel nature of the language.
Finally, we briefly touch on notions of program equivalence in the adjoint setting, which has application both to the development of dependent adjoint types (where a suitable notion of program equivalence is needed to check for type equality), as well as for reasoning about programs and program transformations, for instance in the context of optimizing compilation.
Thesis Committee:
Frank Pfenning (Chair)
Stephanie Balzer
Henry DeYoung
Robert Harper Andrew Pitts (University of Cambridge, Emeritus)
In Person and Zoom Participation. See announcement.