Henry DeYoung

Session-Typed Ordered Logical Specifications Degree Type: Ph.D. in Computer Science
Advisor(s): Frank Pfenning
Graduated: December 2020

Abstract:

Concurrent systems are ubiquitous, but notoriously difficult to get right: subtle races and deadlocks can lurk even in the most extensively tested of systems. In a quest to tame concurrency, researchers have successfully applied the principle of computation as deduction to concurrency in two distinct way: concurrent as proof reduction and concurrency as proof construction. These two approaches to concurrency have complementary advantages, with the proof-construction approach excelling at global specification of a system's dynamics, while the proof-reduction approach is best suited to implementation of the processes that comprise the system.

This document explores the relationship between these two different proof-theoretic characterizations of concurrency. To focus on the essential aspects of their relationship, the exploration is carried out in the context of concurrent systems that have chain topologies. From a proof-construction perspective, chain topologies arise from ordered logic; from a proof-reduction perspective, they arise from singleton logic, a variant of ordered logic that restricts sequents to have exactly one antecedent.

In this context, a rewriting framework is systematically derived from the ordered sequent calculus, and a message-passing fragment of that rewriting framework is identified. String rewriting specifications of concurrent systems can be choreographed into this fragment, and the fragment supports a notion of bisimilarity. Along the way, we also uncover a semi-axiomatic sequent calculus for singleton logic, which blends a standard sequent calculus with axiomatic aspects of Hilbert systems, and we then establish a correspondence between semi-axiomatic proof normalization and asynchronous message-passing communication. Ultimately, the message-passing processes can be faithfully embedded within the message-passing ordered rewriting framework in a bisimilar way. Perhaps surprising is that, because the embedding is left-invertible, we can also identify fairly broad conditions under which local, process implementations can be extracted from global, message-passing ordered rewriting specifications.

Thesis Committee:
Frank Pfenning (Chair)
Iliano Cervesato
Robert Harper
André Platzer
Simon Gay (University of Glasgow)
Carsten Schürmann (IT University of Copenhagen)

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

Keywords:
Concurrency, bisimilarity, session types, proof construction, proof reduction, ordered logic, singleton logic