Cylindric Kleene Lattices for Program Construction

ABSTRACT. Cylindric algebras have been developed as an algebraisation of equational first order logic. We adapt them to cylindric Kleene lattices and their variants and present relational and relational fault models for these. This allows us to encode frames and local variable blocks, and to derive Morgan's refinement calculus as well as an algebraic Hoare logic for while programs with assignment laws. Our approach thus opens the door for algebraic calculations with program and logical variables instead of domain-specific reasoning over concrete models of the program store. Refinement proofs for small programs are presented as examples.

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning

ABSTRACT. One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly because it is difficult to maintain pencil-and-paper proofs of large examples. We propose a formalization of a hierarchy of effects using monads in the Coq proof assistant that makes equational reasoning practical. Our main idea is to formalize the hierarchy of effects and algebraic laws like it is done when formalizing hierarchy of traditional algebras. We can then take advantage of the sophisticated rewriting capabilities of Coq to achieve concise proofs of programs. We also show how to ensure the consistency of our hierarchy by providing rigorous models. We explain the various techniques we use to formalize a rich hierarchy of effects (with nondeterminism, state, probability, and more), to mechanize numerous examples from the literature, and we furthermore discuss extensions and new applications.

ABSTRACT. System F, also known as the polymorphic λ-calculus, is a typed λ-calculus independently discovered by the logician Jean-Yves Girard and the computer scientist John Reynolds. We consider Fωμ, which adds higher-order kinds and iso-recursive types. We present the first complete, intrinsically typed, executable, formalisation of System Fωμ that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System Fωμ. The paper is a literate Agda script.

ABSTRACT. Interactive theorem provers provide the highest possibly correctness guarantee on mathematical proofs. They are designed to help their users formalize and verify mathematical proofs. In the area of program verification, they are used today in top research publications, in the classroom, as well as in widely deployed industrial products. But the software of computer-aided mathematics, like computer algebra systems or numerical scientific computing software, remains as of today largely untouched by this nature of formal methods. In fact, proof assistants themselves even lack the computing functionalities of a standard scientific calculator. In this talk we will discuss some specific pitfalls pertaining to the verification of computer mathematics.

ABSTRACT. Graph-searching algorithms typically assume that a node is given from which the search
begins but in many applications it is necessary to search a graph repeatedly until all nodes in the graph
have been ``visited''. Sometimes a priority function is supplied to guide the choice of node when
restarting the search, and sometimes not. We call the nodes from which a search of a graph is
(re)started the ``delegate'' of the nodes found in that repetition of the search and we analyse the properties
of the delegate function. We apply the analysis to establishing the correctness of the second phase of the
Kosaraju-Sharir algorithm for computing strongly connected components of a graph.

Shallow Embedding of Type Theory Is Morally Correct

ABSTRACT. There are multiple ways to formalise the metatheory of type theory. For some
purposes, it is enough to consider specific models of a type theory, but
sometimes it is necessary to refer to the syntax, for example in proofs
of canonicity and normalisation. One option is to embed the syntax deeply, by
using inductive definitions in a proof assistant. However, in this case the
handling of definitional equalities becomes technically
challenging. Alternatively, we can reuse conversion checking in the metatheory
by shallowly embedding the object theory. In this paper, we consider
the standard model of a type theoretic object theory in Agda. This model
has the property that all of its equalities hold definitionally, and we can use
it as a shallow embedding by building expressions from the components of this
model. However, if we are to reason soundly about the syntax with this setup, we
must ensure that distinguishable syntactic constructs do not become provably
equal when shallowly embedded. First, we prove that shallow embedding is
injective up to definitional equality, by modelling embedding as a syntactic
translation targeting the metatheory. Second, we use an implementation hiding
trick to disallow illegal propositional equality proofs and constructions which
do not come from the syntax. We showcase our technique with very short
formalisations of canonicity and parametricity for Martin-Löf type theory. Our
technique only requires features which are available in all major proof
assistants based on dependent type theory.