This talk will present ongoing work towards the description and study of concurrent interaction in proof theory.

Type systems that are designed to ensure behavioural properties of concurrent processes (input/output regimes, lock-freeness) generally have unclear logical meanings. Conversely, proofs-as-programs correspondences for processes (e.g. with session types) tend to impose very functional behaviour and little actual concurrency. Besides, relationships between type systems and denotational models of concurrency are rarely established.

A possible reason for this state of things is the ambiguous status of non-determinism in logic and the importance of scheduling concerns in models of concurrency, to which traditional proof theory is not accustomed. Unifying logical approaches in a consistent framework requires to put a focus on these issues, and this talk will propose, building on recent developments in proof theory, in the veins of linear logic and classical realizability.

We give a new syntax independent definition of the notion of a finitely presented generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structure. To this end we define inductively how to build a valid signature \(\Sigma\) for a generalized algebraic theory and the associated category \(\textrm{CwF}_{\Sigma}\) of cwfs with a \(\Sigma\)-structure and cwf-morphisms that preserve \(\Sigma\)-structure on the nose. Our definition refers to the purely semantic notions of uniform family of contexts, types, and terms. Furthermore, we show how to syntactically construct initial cwfs with \(\Sigma\)-structures. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of dependent type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual categories with families.

One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic properties. This perspective suggests that, even in the case of quantum algorithms, the control flow notions of sequencing, conditionals, loops, and recursion are entirely classical. There is however, another notion of control flow, that is itself quantum. This purely quantum control flow is however not well-understood. In this talk, I will discuss how to retrieve some understanding of it with a detour through reversible computation. This will allow us to draw links with the logic \(\mu\)MALL, pointing towards a Curry-Howard isomorphism.

We examine recursive monotonic functions on the Lindenbaum algebra of EA. We prove that no such function sends every consistent \(\varphi\), to a sentence with deductive strength strictly between \(\varphi\) and \(\textit{Con}(\varphi)\). We generalize this result to iterates of consistency into the effective transfinite. We then prove that for any recursive monotonic function \(f\), if there is an iterate of \(\textit{Con}\) that bounds \(f\) everywhere, then \(f\) must be somewhere equal to an iterate of \(\textit{Con}\).

Presheaves are an ubiquitary model construction used everywhere in logic, particularly in topos theory. It is therefore tempting to port them to the similar but slightly different context of type theory. Unfortunately, it turns out that there are subtle issues with the built-in computation rules of the latter, which we will expose. As an alternative, we will describe a new structure that is much better behaved in an intensional setting, but categorically equivalent to presheaves in an extensional one. Such a structure is motivated by considerations stemming from the study of generic side-effects in programming language theory, shedding a new light on the fundamental nature of such a well-known object.

The development of computer-checked formal proofs is a major step forward in the endless quest for mathematical rigor. But it also has a negative aspect: the multiplicity of systems brought a multiplicity of theories in which these formal proofs are expressed. We propose to define these theories in a common logical framework, called Dedukti. Some axioms are common to the various theories and some others are specific, just like some axioms are common to all geometries and some others are specific. This logical framework extends predicate logic in several ways and we shall discuss why predicate logic must be extended to enable the expression of these theories.

Everyone has an intuitive idea about what is randomness, often associated with ``gambling'' or ``luck''. Is there a mathematical definition of randomness? Are there degrees of randomness? Can we give examples of randomness? Can a computer produce a sequence that is truly random? What is the relation between randomness and logic? In this talk I will talk about these questions and their answers.