Rencontre, 9 novembre 2017
Programme
- 10:30 – 12:00
-
Laura Fontanella (I2M, Aix-Marseille)Invited talk: Realizability: from Curry-Howard to forcing
Realizability studies the computational content of proofs by defining a correspondence between the formulas of a logical system and programs in such a way that knowledge of the “realizers” (i.e. the programs associated with the formula) gives information about the proof of the formula. The Curry-Howard isomorphism establishes a correspondence between proofs of intuitionistic logic formulas and programs seen as lambda-terms. The scope of Realizability was later extended to classical logic thanks to the work by Griffin on typing operators. Thanks to Krivine, research in realizability further evolved to encompass proofs in set theory. The technique developed by Krivine generalizes the method of forcing in set theory, in fact forcing models are special cases of realizability models. This talk is meant as a gentle introduction to Forcing from the point of view of classical realizability.
- 14:00 – 15:00
-
Jules Chouquet (IRIF, Univ. Paris Diderot)
We study the behaviour of the cut elimination in differential linear logic proof nets (without exponential boxes).
Sometimes, we want to consider parallel reduction, that fires as much cuts as wanted in the net, but doing so, we are not able to bound the loss of size in one step of reduction. We propose a method (adapted from a Lionel Vaux technique in lambda calculus) where, recovering a kind of geometric invariant in proof nets, allows us to manage this loss of size. We are then able, with well-chosen informations, to bound the size of all possible antireducts of a given net.
This result leads to others, since the notion of invariance we're dealing with can be applied to infinite sets of structures, like the Taylor expansions of nets. In this setting, we deduce from the geometrical considerations above, an interesting finiteness result having at least two nice applications : one concerning the simulation of the exponential cut-elimination in MELL; one concerning a normalization by evaluation method in connected MELL proof-nets.
- 15:30 – 16:30
-
Thomas Seiller (DIKU, Univ. Copenhagen)Invited talk: Towards a geometric theory of computation(al complexity)
The purpose of this talk is to explain a new approach to complexity theory based on (dynamic) semantics of linear logic, whose aim is to enable techniques and invariants from ergodic theory (e.g. l^2-Betti numbers of a countable Borel equivalence relation) to be used in computational complexity.
The origins of the techniques can be traced to Girard's “geometry of interaction” (GoI) program using von Neumann algebras and the recent GoI-inspired results in complexity. However, this approach reaches its full strength when using the more combinatorial setting of Interaction Graphs models of (fragments of) linear logic. Using techniques akin to game semantics (with a bit of measure theory), we are able to characterise (predicate) complexity classes as the set of programs/proofs interpretations of type Pred[m] := Nat ⇒ Bool. These models are parametrised by a group of measure-preserving maps m (equivalently, by a measurable group action) and provide the first sketches of a conjectured correspondence between measurable group/monoid actions and complexity constraints.
