Computer Science Thesis Oral
- Remote Access - Zoom
- Virtual Presentation
- HENRY DAVID DeYOUNG
- Ph.D. Student
- Computer Science Department
- Carnegie Mellon University
Session-Typed Ordered Logical Specifications
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 ways: concurrency as proof construction and concurrency as proof reduction. 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 thesis 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 are arranged in chain configurations. From a proof-construction perspective, chain configurations 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 cut reduction 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.
Frank Pfenning (Chair)
Simon Gay (University of Glasgow)
Carsten Schürmann (IT University of Copenhagen)
Zoom Participation. See announcement.