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 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.