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.

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.

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.