We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [Aspnes, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.

Given an irrational number $\alpha$, we study the asymptotic behaviour of the Sudler product defined by $P_N(\alpha) = \prod_{r=1}^N 2 \lvert \sin \pi r \alpha \rvert$, which appears in many different areas of mathematics. In this talk, we explain the connection between the size of $P_N(\alpha)$ and the Ostrowski expansion of $N$ with respect to $\alpha$. We show that $\liminf_{N \to \infty} P_N(\alpha) = 0$ and $\limsup_{N \to \infty} P_N(\alpha)/N = \infty$, whenever the sequence of partial quotients in the continued fraction expansion of $\alpha$ exceeds $7$ infinitely often, and show that the value $7$ is optimal.

For Lebesgue-almost every $\alpha$, we can prove more: we show that for every non-decreasing function $\psi: (0,\infty) \to (0,\infty)$ with $\sum_{k=1}^{\infty} \frac{1}{\psi(k)} = \infty$ and $\liminf_{k \to \infty} \psi(k)/(k \log k)$ sufficiently large, the conditions $\log P_N(\alpha) \leq -\psi(\log N)$, $\log P_N(\alpha) \geq \psi(\log N)$ hold on sets of upper density $1$ respectively $1/2$.

Longest Common Substring (LCS) is an important text processing problem, which has recently been investigated in the quantum query model. The decisional version of this problem, LCS with threshold d, asks whether two length-n input strings have a common substring of length d. The two extreme cases, d = 1 and d = n, correspond respectively to Element Distinctness and Unstructured Search, two fundamental problems in quantum query complexity. However, the intermediate case 1 « d « n was not fully understood.

We show that the complexity of LCS with threshold d smoothly interpolates between the two extreme cases up to n^{o(1)} factors: LCS with threshold d has a quantum algorithm in n^{2/3 + o(1)}/d^{1/6} query complexity and time complexity, and requires at least Omega(n^{2/3}/d^{1/6}) quantum query complexity.

Our result improves upon previous upper bounds O~(min{ n/d^{1/2}, n^{2/3} }) (Le Gall and Seddighin ITCS 2022, Akmal and Jin SODA 2022), and answers an open question of Akmal and Jin.

Our main technical contribution is a quantum speed-up of the powerful String Synchronizing Set technique introduced by Kempa and Kociumaka (STOC 2019). Our quantum string synchronizing set also yields a near-optimal LCE data structure in the quantum setting, and an algorithm for the k-mismatch matching problem with k^{3/4}n^{1/2+o(1)} quantum query complexity.

Based on a SODA'23 paper joint with Jakob Nogler (ETH Zurich) and a SODA'22 paper joint with Shyan Akmal (MIT).

Obfuscation transforms a program C into a functionally equivalent program C' which hides the inner workings of C. The first formalizations of this hiding property in cryptography suffered from strong impossibility results and thus, the seemingly weak notion of indistinguishability obfuscation (iO) was formulated. It only requires that obfuscations of two circuits are indistinguishable when two circuits have equal functionality to begin with.

Although iO seems such a weak definition, it turns out surprisingly powerful (*). It allows us to transform worst-case NP problems into one-way functions, one-way functions into public-key encryption and even into fully homomorphic encryption—transformations which otherwise suffer from (black-box) separations result. In fact, iO is so strong that its existence is mutually exclusive with other assumptions which had previously been considered plausible.

At the same time, iO is also very weak; it does not even imply that P is different from NP although most cryptographic primitives (one-way functions, public-key encryption etc.) do.

In this talk, we explore the above conceptual implications. The talk is intended for a (broad) theory audience.

(*) “I must admit that I was very skeptic of the possible applicability of the notion of indistinguishable obfuscation.” Oded Goldreich when commenting on the surprising success of iO in cryptographc research.

The goal of this talk is to present the article “Geometry of the $nu$-Tamari lattices in types A and B”, by Cesar Ceballos, Arnau Padrol, Camilo Sarmiento. We will present the nu-Tamari lattice, a generalization of the Tamari lattice where the parameter $nu$ is a lattice path. One incarnation of the nu-Catalan objects is given by the lattice paths weakly above nu. We will explain briefly how certain nu-Tamari lattices partition the usual Tamari lattice. We will focus on the geometric realization of this lattice as a triangulation of a certain polytope. This relies on another incarnation of nu-Catalan objects, the (I, J)-trees introduced by Ceballos-Padrol-Sarmiento.

The subject of this thesis is the proof theory of linear logic with the least and greatest fixed points. In the literature, several systems have been studied for this language viz. the wellfounded system that relies on Park's induction rule, and systems that implicitly characterise induction such as the circular system and the non-wellfounded system. This thesis contributes to the theory of these systems with the ultimate goal of exactly capturing the provability relation of these systems and application of these objects in programming languages supporting (co)inductive reasoning. This thesis contains three parts. In the first part, we recall the literature on linear logic and the main approaches to the proof theory of logics with fixed points. In the second part, we obtain truth semantics for the wellfounded system, devise new wellfounded infinitely branching systems, and compute the complexity of provability in circular and non-wellfounded systems. In the third part, we devise non-wellfounded proof-nets and study their dynamics.

Manuscript

(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.

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.