There are well-known dualities of computation in both functional and concurrent programming: input/output, expression/context, strict/lazy, sender/receiver, forward/backwards, and several others. When viewed through an algebraic lens, these can be understood as metaphysical interpretations of rigorous mathematical dualities.

In this talk, I will explore the duality of values and continuations (Filinski'89) through the lens of cartesian closure/co-cartesian co-closure. The main observation is that, just as higher-order functions give exponentials, higher-order continuations give co-exponentials. Using this semantic duality, I will present a λλ~ (lambda-lambda-bar or tilde) calculus, which exhibits a duality of abstraction/co-abstraction. I will develop the syntax and semantics of this language, which gives a computational interpretation in terms of speculative execution and backtracking.

Using this language, I will show how to recover classical control operators, the computational interpretation of classical logic, and a complete axiomatisation of control effects. Finally, I will show how this dualises Lambek's functional completeness, thereby dualising Hasegawa's decomposition of λ-calculus into first-order κ/ζ-calculi.

Given a matrix $A$ with $m$ rows and $n$ columns, we want to approximate the maximum value of $||A x||_p$ when $||x||_q <= 1$. For general matrices, a $(1-\epsilon)$ approximation of the problem is hard, but for nonnegative matrices, when $q >= p >= 1$, the problem can be transformed into a concave maximization problem. In this talk, we will present a width-independent (i.e., the running time dependence on $n m$ is at most poly-logarithmic) algorithm to find $(1-\epsilon$) approximations in time nearly $O(nnz/\epsilon)$.

In the second part of the talk, we will see how such an algorithm can be used to compute competitive oblivious linear routings.

We consider the context of a network modeled by an undirected graph where the edges are known, but not the connections between these edges. This can happen in old buildings where, for example, an electrical, gas or water network has not been documented and where the network is not easily accessible. We may have access to some cables or pipes of the network either because they are visible or because it is possible to probe the building to find them. From the edges of the graph, we obtain measures of the probability that two edges are incident, in other words measures of the linegraph of the network, with possibly errors in the measurements. We aim to correct the errors by finding the linegraph closest to the measurement graph. This problem is modeled as an edit distance problem in terms of deleting and adding edges in a graph to retrieve a linegraph. We pose the question, firstly, of studying the complexity of correcting these errors and its parameterized complexity with respect to the number of possible errors and the treewidth of the graph, secondly, the relevance of such correction in relation to the desired graph based on the number of measurement errors, and thirdly, what other information could be added to the graph to aid in reconstruction as the number of measurement errors increases.

Since artificial intelligence is nowadays also increasingly applied in safety-critical applications such as autonomous driving and human robot collaboration, there is an urgent need for approaches that can efficiently verify that the corresponding neural networks are safe. In general, verification tasks involving neural networks can be classified into the two groups open-loop verification and closed-loop verification. For open-loop verification one aims to prove certain properties of a standalone neural network, while for closed-loop verification the neural network acts as a controller for a dynamic system. This presentation demonstrates a novel verification technique that is based on a polynomial abstraction of the input-output-relation of the single neurons, which proves to be beneficial for both open- as well as closed-loop neural network verification.

One of the founding results of lattice based cryptography is a quantum reduction from the Short Integer Solution (SIS) problem to the Learning with Errors (LWE) problem introduced by Regev. It has recently been pointed out by Chen, Liu and Zhandry [CLZ22] that this reduction can be made more powerful by replacing the LWE problem with a quantum equivalent, where the errors are given in quantum superposition. In parallel, Regev’s reduction has recently been adapted in the context of code-based cryptography by Debris, Remaud and Tillich [DRT23], who showed a reduction between the Short Codeword Problem and the Decoding Problem (the DRT reduction). This motivates the study of the Quantum Decoding Problem (QDP), which is the Decoding Problem but with errors in quantum superposition and see how it behaves in the DRT reduction.

The purpose of this paper is to introduce and to lay a firm foundation for QDP. We first show QDP is likely to be easier than classical decoding, by proving that it can be solved in quantum polynomial time in a large regime of noise whereas no non-exponential quantum algorithm is known for the classical decoding problem. Then, we show that QDP can even be solved (albeit not necessarily efficiently) beyond the information theoretic Shannon limit for classical decoding. We give precisely the largest noise level where we can solve QDP giving the information theoretic limit for this new problem. Finally, we study how QDP can be used in the DRT reduction. First, we show that our algorithms can be properly used in the DRT reduction showing that our quantum algorithms for QDP beyond Shannon capacity can be used to find minimal weight codewords in a random code. On the negative side, we show that the DRT reduction cannot be, in all generality, a reduction between finding small codewords and QDP by exhibiting quantum algorithms for QDP where this reduction entirely fails. Our proof techniques include the use of specific quantum measurements, such as q-ary unambiguous state discrimination and pretty good measurements as well as strong concentration bounds on weight distribution of random shifted dual codes, which we relate using quantum Fourier analysis.

A temporal graph is an undirected graph G = (V,E) along with a function that assigns a time-label to each edge in E. A path in G such that the traversed time-labels are non-decreasing is called a temporal path. Accordingly, the distance from u to v is the minimum number of edges of a temporal path from u to v. A temporal alfa-spanner of G is a (temporal) subgraph H that preserves the distances between any pair of vertices in V, up to a multiplicative stretch factor of alfa. The size of H is measured as the number of its edges. In this work, we study the size-stretch trade-offs of temporal spanners. In particular we show that temporal cliques always admit a temporal (2k-1)-spanner with \tilde{O}(kn^{1+1/k}) edges, where k > 1 is an integer parameter of choice and n is the number of nodes in G. Choosing k = log n, we obtain a temporal O(log n)-spanner with \tilde{O}(n) edges that has almost the same size (up to logarithmic factors) as the temporal spanner given in [Casteigts et al., JCSS 2021] to preserve temporal connectivity. We then turn our attention to general temporal graphs. Since \Omega(n^2) edges might be needed by any connectivity-preserving temporal subgraph [Axiotis et al., ICALP'16], we focus on approximating distances from a single source. We show that \tilde{O}(n/log(1+epsilon)) edges suffice to obtain a stretch of (1+epsilon), for any small epsilon > 0. This result is essentially tight in the following sense: there are temporal graphs G for which any temporal subgraph preserving exact distances from a single-source must use \Omega(n^2) edges.

I will present a type system based on non-idempotent intersection types for PCFh, a variant of PCF. Evaluation in PCFh is hybrid: call-by-name (CBN) and call-by-value (CBV) behaviours cohabit together. Specifically, function application follows CBV semantics, while recursion has a CBN flavour. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFh evaluation. This means not only that typability implies normalisation, but also that the converse holds. Moreover, the type system is quantitative, since the size of typing derivations provides upper bounds for the length of normalisation sequences. By refining this type system, we obtain a tight type system, which offers exact information regarding the length of normalisation sequences.