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 computationally complete symbolic attacker (CCSA) is a logically-based approach proposed by Bana and Comon to verify cryptographic protocols in the computational model, i.e. in the model of cryptographers where messages are probabilistic bitstrings and attackers are arbitrary probabilistic PTIME machines. The original formulation of CCSA was based on first-order logic and only supported the verification of protocols with bounded traces. With several co-authors, we have proposed in 2020 to build a meta-logic on top of this “base” first-order logic, to obtain a methodology that supports verifying unbounded protocols. This meta-logic forms the basis of the Squirrel proof assistant.

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

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.