Reporting on recent results of joint work with R. Harmer, P.-A. Melliès and N. Zeilberger, I will present a novel formalization of compositional rewriting theory via double categories. For a given rewriting theory, individual rewriting steps are formalized as 2-cells of a double category. One of the crucial aspects of compositionally consists then in providing a set of axioms that the double category of the rewriting system must satisfy in order to ensure the existence of concurrency and associativity theorems, which are quintessential for developing important applications of rewriting systems such as in combinatorics and Markov chain theory. Another concept central to this end, i.e., “counting modulo universal properties”, may be implemented via a certain presheaf and coend calculus. Finally, I will sketch how the counting calculus then leads to a categorification of the concept of rule algebras (which capture the combinatorics of interactions of rewriting steps).

Runtime verification consists in checking whether a program satisfies a given specification by observing the trace it produces during its execution. In the regular setting, Hennessy-Milner logic with recursion (recHML), a variant of the modal $\mu$-calculus, provides a versatile back-end for expressing linear- and branching-time specifications. In this talk, I will discuss an extension of this logic that allows to express properties over data values (i.e. values from an infinite domain) and examine which fragments can be verified at runtime. Data values are manipulated through equality tests in modalities and through first-order quantification outside of them. They can also be stored using parameterised recursion variables.

I then examine what kind of properties can be monitored at runtime, depending on the monitor model. A key aspect is that the logic has close links with register automata with non-deterministic reassignment, which yields a monitor synthesis algorithm, and allows to derive impossibility results. In particular, contrary to the regular case, restricting to deterministic monitors strictly reduces the set of monitorable properties.

This is joint work with the MoVeMnt team (Reykjavik University): Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Adrian Francalanza, Karoliina Lehtinen.

(Joint work with Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, and Atsushi Igarashi)

A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This article describes our type-based static verification tool HELMHOLTZ for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. HELMHOLTZ is designed on top of our extension of Michelson's type system with refinement types. HELMHOLTZ takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. HELMHOLTZ successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.

In this talk, I will introduce a recent work with Ashley Montanaro. I will show you that quantum computers can have exponential speedups in terms of communication complexity for some fundamental linear algebra problems. I will mainly introduce our results on solving linear regressions. The talk is based on arXiv:2210.01601.

This talk is about the semantics of commutative combinations of effects.

A basic class of effects comes from the algebraic theory of modules for a semiring. The tensor of such theories is determined by the usually more tractable semiring tensor. I’ll give some examples, and then look at how the tensors work in languages with iteration. Our main contribution concerns an important class of subtheories of module theories. We observe that the subtheory tensor is also determined by the semiring tensor for several fundamental effects. I'll look at some examples of these subtheories and their tensors, and discuss how they support iteration via the underlying subsets.

This is my undergraduate summer project with Cristina Matache, Sean Moss, and Sam Staton.

Numeration assigns symbolic sequences as addresses to points in a space X. There are points which get multiple addresses. It is known that these identifications describe the topology of X and can often be determined by an automaton. Here we define a corresponding class of automata and discuss their properties and interesting examples. Various open questions concern the realization of such automata by iterated functions and the uniqueness of such an implementation. Self-affine tiles form a simple class of examples.

Kyber is a key-encapsulation mechanism (KEM), whose security is based on the hardness the Module-LWE problem. It is the only KEM that has been selected by the NIST Post-Quantum Cryptography project, and will be part of NIST’s first post-quantum cryptography standard. Hakyber, a formally verified implementation of Kyber, has been developed. Hakyber is written in Jasmin, and formally verified in EasyCrypt.

EasyCrypt has already been used to prove the correction of implementations of cryptographic primitives, such as of ChaCha20-Poly1305. This proof is done by “game hopping”: the correction of a naive implementation of the primitive is proven using EasyCrypt’s probabilistic Hoare logic (pHL), and it is shown to be equivalent to gradually more optimized implementations using EasyCrypt’s probabilistic relational Hoare logic (pRHL).

Hakyber differs from the cryptographic primitives formalized in EasyCrypt by the complexity of the mathematical structures involved in it’s correctness an security proofs. In particular, it’s correction proof involves polynomials over finite fields, quotient rings and Number Theoretic Transforms (NTTs), variants of the Fourier transform used in fast polynomial multiplication algorithms.

The correction proof of Hakyber’s NTT is one of the trickiest parts of the total correction proof. We will discuss the issues we encountered in this proof, the solutions we used to overcome them, and current and planned developments of EasyCrypt that were motivated by these issues.

In particular, we will talk about the theories developed to deal with equivalence proofs of nested for loops, as well as those describing algebraic hierarchies using EasyCrypt’s clone mechanism. We will then present the planned replacement for these theories, using EasyCrypt’s annotations and type class mechanism respectively.

The theory of cluster algebras, introduced twenty years ago by Fomin and Zelevinsky, gives us a combinatorial framework for understanding the previously opaque nature of certain algebras. Each cluster algebra is generated by its cluster variables, which are defined recursively via the process of mutation. In the rank two case, several explicit formulas have been given for the cluster variables in terms of combinatorial, representation theoretic, and tropical objects. We will focus on two such formulas. The first, given by Lee-Schiffler, sums over collections of colored Dyck subpaths, and the second, given by Lee-Li-Zelevinsky, sums over compatible pairs in Dyck paths. We will discuss a correspondence between these two sets of objects, as well as a simplification and quantum generalization of the Lee-Schiffler expansion formula.

In this talk, I will start by discussing the lack of a reasonable time cost model for linear logic. Then, inspired by recent advances in the sister field of lambda calculus, I will introduce a new term-based presentation of cut elimination for IMELL admitting a reasonable strategy (that is, a strategy of which the number of step is a reasonable time cost model). The focus will be on the principles behind the new presentation of cut elimination.

I will introduce some consensus protocols and give an overview of some of the implementations. Following that, I will introduce what are the existing approaches to testing the implementations and then explain our approach which is akin to unit testing.

No prior knowledge of distributed systems/algorithms is required.