Abstracts

Alejandro Díaz-Caro

Title: Towards a computational quantum logic

Abstract: This talk provides an overview of a long-term collaboration with Octavio Malherbe (UdelaR) and Gilles Dowek (INRIA, Saclay) aimed at extending the Curry-Howard-Lambek correspondence to the realm of quantum computation. I will introduce the Lambda-S calculus, a dual to intuitionistic linear logic whose proof terms serve as a foundation for a quantum programming language. Additionally, I will discuss the L-S calculus, a proof language for intuitionistic linear logic, which also enables the construction of quantum programming languages. These frameworks offer a logical and computational foundation for reasoning about quantum programs and provide a glimpse into the structure of a potential quantum logic as the dual of linear logic.

Mariana Millicich

Title: Useful call-by-value, quantitatively

Abstract: Useful evaluation (Accattoli and Dal Lago, 2016) is an optimised evaluation mechanism for functional programming languages. The key of useful evaluation is to represent programs with sharing, and to implement substitution of terms only when this contributes to the progress of the computation. The definitions of usefulness in the literature are complex and lack inductive structure, which makes it challenging to (formally) reason about them. In particular, there are no semantic model of usefulness to this day.

The main focus of this talk is to present the first semantic model of useful call-by-value evaluation, by means of a quantitative type system called system U. To obtain such type system, a key step was to define inductively useful evaluation within call-by-value, yielding the UCBV strategy. Substitution in useful evaluation is sensitive to the surrounding evaluation context, so defining UCBV is not trivial. Our main result is a characterisation of termination for useful call-by-value evaluation via system U. That is, a term t terminates in useful call-by-value if and only if t types in system U. Additionally, system U provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Even though the specification of the operational semantics of useful evaluation is highly complex, system U is notably simple. As far as we know, system U is one of the scarce quantitative type systems capturing exactly the substitution step-count for a call-by-value strategy.

Marin Costes

Title: Space-time deterministic graph rewriting

Abstract: We study non-terminating graph rewriting models, whose local rules are applied non-deterministically -- and yet enjoy a strong form of determinism, namely space-time determinism. Of course in the case of terminating computation it is well-known that the mess introduced by asynchronous rule applications may not matter to the end result, as confluence conspires to produce a unique normal form. In the context of non-terminating computation however, confluence is a very weak property, and (almost) synchronous rule applications is always preferred e.g. when it comes to simulating dynamical systems. Here we provide sufficient conditions so that asynchronous local rule applications conspire to produce well-determined events in the space-time unfolding of the graph, regardless of their application orders. Our first example is an asynchronous simulation of a dynamical system. Our second example features time dilation, in the spirit of general relativity.

Fabio Gadducci

Title: Testing Quantum Processes

Abstract: Several quantum process calculi and behavioural equivalences have been recently proposed, but they are often incompatible with the prescriptions of quantum theory, as they implicitly define omniscient observers that are capable of exactly discriminating the state of a physical system, therefore contradicting the uncertainty principle. In this talk we address these observational limitations by resorting to testing equivalence for a quantum capable version of CCS, building on the concrete actions and experiments that a real tester can perform.

Mauricio Guillermo

Title: Concurrent realizability on conjunctive structures

Abstract: This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in the realm of classical and intuitionistic realizability. In particular, we show how any CIMA provides a sound interpretation of multiplicative linear logic MLL. This new structure involves, in addition to the tensor ⊗ and the orthogonal map (·)⊥ , a parallel composition |. We define the canonical model of this structure as induced by a variant of the π-calculus with global fusions. Using a model of terms, we prove that the parallel composition cannot be defined from the conjunctive structure alone.

Claudio Antares Mezzina

Title: Reversibility in process calculi with nondeterminism and probabilities

Abstract: A reversible system features not only forward computations, but also backward computations along which the effects of forward ones can be undone by starting from the last performed action. According to causal reversibility, an executed action can be undone provided that all the actions it caused have been undone already. We investigate causal reversibility in a nondeterministic and probabilistic setting by adapting the framework of Phillips and Ulidowski to define a reversible calculus in which action transitions and probabilistic transitions alternate in the style of Hansson and Jonsson. We show that the calculus meets causal reversibility through a suitable variant of the technique of Lanese, Phillips, and Ulidowski that ensures the proper forward and backward interplay of nondeterminism and probabilities. The use of the calculus is illustrated on a quantum computing example.