ABSTRACT. Formal methods are invaluable for reasoning about complex systems. As these techniques and tools have improved in expressiveness and scale, their adoption has grown rapidly. Sustaining this growth, however, requires attention to not only the technical but also the human side. In this paper (and accompanying talk), we discuss some of the challenges and opportunities for human factors in formal methods.

ABSTRACT. Reversible computation studies computations which exhibit both forward and backward determinism. Among others, it has been studied for half a century for its applications in low-power computing, and forms the basis for quantum computing.

Though certified program equivalence is useful for a number of applications (e.g., certified compilation and optimization), little work on this topic has been carried out for reversible programming languages. As a notable exception, Carette and Sabry have studied the equivalences of the finitary fragment of Πo, a reversible combinator calculus, yielding a two-level calculus of type isomorphisms and equivalences between them.

In this paper, we extend the two-level calculus of finitary Πo to one for full Πo (i.e., with both recursive types and iteration by means of a trace combinator) using the delay monad, which can be regarded as a ``computability-aware'' analogue of the usual maybe monad for partiality. This yields a calculus of iterative (and possibly nonterminating) reversible programs acting on user-defined dynamic data structures together with a calculus of certified program equivalences between these programs.

ABSTRACT. Synchronous Kleene algebra SKA, an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. the language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then propose an alternative set of axioms for SKA, based on Salomaa's axiomatisation of regular languages, and show that these provide a sound and complete characterisation w.r.t. the original language semantics.

ABSTRACT. Lambda calculi are often used as intermediate representations for compilers. However, they require extensions to handle higher-level features of programming languages. In this paper we show how to construct an IR based on System F_{\omega}^{\mu} which supports recursive functions and datatypes, and describe how to compile it to System F_{\omega}^{\mu}. Our IR was developed for commercial use at the IOHK company, where it is used as part of a compilation pipeline for smart contracts running on a blockchain.

ABSTRACT. Asymmetric Numeral Systems (ANS) are an entropy-based encoding method introduced by Jarek Duda, combining the Shannon-optimal compression effectiveness of arithmetic coding with the execution efficiency of Huffman coding. Existing presentations of the ANS encoding and decoding algorithms are somewhat obscured by the lack of suitable presentation techniques; we present here an equational derivation, calculational where it can be, and highlighting the creative leaps where it cannot.