On incorrectness logic and Kleene algebra with top and tests

Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by O'Hearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT.

Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages

The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, forming an equivalence of groupoids. We use this to establish a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and bijections. Using the formalisation of our results, we perform normalisation-by-evaluation, verification and synthesis of reversible logic gates, motivated by examples from quantum computing. We also show how to reason about and transfer theorems between different representations of reversible circuits.

Modular, compositional, and executable formal semantics for LLVM IR

This paper presents a novel formal semantics, mechanized in Coq, for a large, sequential subset of the LLVM IR. In contrast to previous approaches, which use relationally-specified operational semantics, this new semantics is based on monadic interpretation of interaction trees, a structure that provides a more compositional approach to defining language semantics while retaining the ability to extract an executable interpreter. Our semantics handles many of the LLVM IR's non-trivial language features and is constructed modularly in terms of event handlers, including those that deal with nondeterminism in the specification. We show how this semantics admits compositional reasoning principles derived from the interaction trees equational theory of weak bisimulation, which we extend here to better deal with nondeterminism, and we use them to prove that the extracted reference interpreter faithfully refines the semantic model. We validate the correctness of the semantics by evaluating it on unit tests and LLVM IR programs generated by HELIX.

A String Diagrammatic Axiomatisation of Finite-State Automata

We develop a fully diagrammatic approach to finite-state automata, based on reinterpreting their usual state-transition graphical representation as a two-dimensional syntax of string diagrams. In this setting, we are able to provide a complete equational theory for language equivalence, with two notable features. First, the proposed axiomatisation is finite— a result which is provably impossible for the one-dimensional syntax of regular expressions. Second, the Kleene star is a derived concept, as it can be decomposed into more primitive algebraic blocks.

Blame and coercion: Together again for the first time

C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop four calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are as follows: $\lambda{B}$ , based on the blame calculus of Wadler and Findler (2009); $\lambda{C}$ , inspired by the coercion calculus of Henglein (1994); $\lambda{S}$ inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006); and $\lambda{T}$ based on the threesome calculus of Siek and Wadler (2010). While $\lambda{B}$ and $\lambda{T}$ are little changed from previous work, $\lambda{C}$ and $\lambda{S}$ are new. Together, $\lambda{B}$ , $\lambda{C}$ , $\lambda{S}$ , and $\lambda{T}$ provide a coherent foundation for design, implementation, and optimization of gradual types. We define translations from $\lambda{B}$ to $\lambda{C}$ , from $\lambda{C}$ to $\lambda{S}$ , and from $\lambda{S}$ to $\lambda{T}$ . Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: $\lambda{C}$ has a particularly simple definition, and the subtle definition of blame safety for $\lambda{B}$ is justified by the simple definition of blame safety for $\lambda{C}$ . Our calculus $\lambda{S}$ is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from $\lambda{C}$ to $\lambda{S}$ to establish an equational theory of coercions; and second, using full abstraction from $\lambda{B}$ to $\lambda{S}$ to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.

Bounded ACh unification

We consider the problem of the unification modulo an equational theory associativity and commutativity (ACh), which consists of a function symbol h that is homomorphic over an associative–commutative operator +. Since the unification modulo ACh theory is undecidable, we define a variant of the problem called bounded ACh unification. In this bounded version of ACh unification, we essentially bound the number of times h can be applied to a term recursively and only allow solutions that satisfy this bound. There is no bound on the number of occurrences of h in a term, and the + symbol can be applied an unlimited number of times. We give inference rules for solving the bounded version of the problem and prove that the rules are sound, complete, and terminating. We have implemented the algorithm in Maude and give experimental results. We argue that this algorithm is useful in cryptographic protocol analysis.

Computing knowledge in equational extensions of subterm convergent theories

We study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system (TRS). In this work, we extend this to consider a subterm convergent TRS defined modulo an equational theory, like Commutativity. We present two pairs of solutions for these important problems. The first solves the deduction and static equivalence problems in rewrite systems modulo shallow theories such as Commutativity. The second provides a general procedure that solves the deduction and static equivalence problems in subterm convergent systems modulo syntactic permutative theories, provided a finite measure is ensured. Several examples of such theories are also given.

Relative Full Completeness for Bicategorical Cartesian Closed Structure

The glueing construction, defined as a certain comma category, is an important tool for reasoning about type theories, logics, and programming languages. Here we extend the construction to accommodate ‘2-dimensional theories’ of types, terms between types, and rewrites between terms. Taking bicategories as the semantic framework for such systems, we define the glueing bicategory and establish a bicategorical version of the well-known construction of cartesian closed structure on a glueing category. As an application, we show that free finite-product bicategories are fully complete relative to free cartesian closed bicategories, thereby establishing that the higher-order equational theory of rewriting in the simply-typed lambda calculus is a conservative extension of the algebraic equational theory of rewriting in the fragment with finite products only.