previous day
all days

View: session overviewtalk overview

09:00-10:00 Session 10: FM Keynote
Location: AWS
The Human in Formal Methods

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.

10:00-10:30Coffee Break
10:30-12:30 Session 11
Location: Miragaia
En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad

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.

Completeness and Incompleteness of Synchronous Kleene Algebra

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.

Unraveling Recursion: Compiling an IR with Recursion to System F

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.

12:30-14:00Lunch Break
14:00-15:00 Session 12
Location: Miragaia
Coding with Asymmetric Numeral Systems

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.

15:00-15:30Coffee Break