ABSTRACT. We were thrilled to know that our PPDP’09 paper “Foundations of Session Types” was selected for the PPDP Most Influential Paper 10-Year Award. Just moments after being notified of this, we couldn’t help looking at the works that cited—and in some cases were inspired by—our own. The result is a short note, in which we recollect the main ideas behind our own work and the related ones that followed. 

ABSTRACT. This paper describes the application of a high-level language and method in developing simpler specifications of more complex variants of the Paxos algorithm for distributed consensus. The specifications are for Multi-Paxos with preemption, replicated state machine, and reconfiguration and optimized with state reduction and failure detection. The language is DistAlgo. The key is to express complex control flows and synchronization conditions precisely at a high level, using nondeterministic waits and message-history queries. We obtain complete executable specifications that are almost completely declarative---updating only a number for the protocol round besides the sets of messages sent and received.

We show the following results: (1) English and pseudocode descriptions of distributed algorithms can be captured completely and precisely at a high level, without adding, removing, or reformulating algorithm details to fit lower-level, more abstract, or less direct languages. (2) We created higher-level control flows and synchronization conditions than all previous specifications, and obtained specifications that are much simpler and smaller, even matching or smaller than abstract specifications that omit many algorithm details. (3) The simpler specifications led us to easily discover useless replies, unnecessary delays, and liveness violations (if messages can be lost) in previous published specifications, by just following the simplified algorithm flows. (4) The resulting specifications can be executed directly, and we can express optimizations cleanly, yielding drastic performance improvement over naive execution and facilitating a general method for merging processes. (5) We systematically translated the resulting specifications into TLA+ and developed machine-checked safety proofs, which also allowed us to detect and fix a subtle safety violation in an earlier unpublished specification. Additionally, we show the basic concepts in Paxos that are fundamental in many distributed algorithms and show that they are captured concisely in our specifications.

ABSTRACT. Rainfall is a smart contract programming model that allows mutually distrusting parties to manage assets on a distributed ledger. The model consists of a tuple space of authorized facts, and a set of production rules. Rules match on authorized facts, gaining their authority, and produce new facts with a subset of the gained authority. Rainfall allows assets such as crypto currencies to be defined in user code, rather than being baked directly into the ledger framework. Our authorization model also provides a natural privacy model, where not all rules or facts need to be revealed to all parties.

ABSTRACT. Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification framework, called Drive, which allows a developer to reason about ETS or other extra-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.

ABSTRACT. Categorical combinators offer a simpler alternative to typed lambda calculi for static analysis and implementation. Since categorical combinators are accompanied by a rich set of conversion rules which arise from categorical laws, they also offer a plethora of opportunities for program optimization. It is unclear, however, how such rules can be applied in a systematic manner to eliminate the use of intermediate values such as exponentials (the categorical equivalent of higher-order functions) from a program built using combinators. Exponential elimination simplifies static analysis and enables a simple closure-free implementation of categorical combinators---reasons for which it has been sought after. In this paper, we prove exponential elimination for bicartesian closed category (BCC) combinators using normalization. We achieve this by showing that BCC terms can be normalized to normal forms which obey a weak subformula property. We implement normalization using Normalization by Evaluation, and also show that the generated normal forms are correct using appropriate logical relations.

ABSTRACT. Landauer's seminal work states that a computation principle can be made reversible by adding the history of the computation, a so-called Landauer embedding, to each state. Although it may seem impractical at first, there are several useful reversibilization techniques that are roughly based on this idea. In this talk, we first introduce a Landauer embedding for a simple (first-order) eager functional language and illustrate its usefulness to define an automatic bidirectionalization technique in the context of bidirectional programming. Then, we extend the language with some primitives for message-passing concurrency and present an appropriate Landauer embedding to make its computations reversible. In this case, we consider reversible debugging as a promising application of reversible computing. Here, the user can explore a computation back and forth in a causal-consistent way (i.e., so that an action is not undone until all the actions that depend on it have already been undone) until the source of a misbehavior is found.