Talks

Jules Chouquet (IRIF, Paris Diderot)
With Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco and Lionel Vaux.
We present a way to bound the size of the antireducts in ressource proofnets (differential nets without boxes), whith respect to the parallel reduction (that is the elimination of an arbitrary number of cuts). This result applies in particular to Taylor expansion of acyclic nets, and leads us to propose a method of normalization by evaluation : we are able to isolate finitely many ressource nets appearing in the relational semantics (that is close to the Taylor expansion) of a net p, and recover its normal form, only whith linear evaluation over these ressource nets.
 Oct. 24, 2017, 12:55 p.m.

Raphaëlle Crubillé
Probabilistic coherence spaces yield a model of linear logic and lambdacalculus with a linear algebra flavor. Formulas/types are associated with convex sets of R + valued vectors, linear logic proofs with linear functions and λterms with entire functions, both mapping the convex set of their domain into the one of their codomain. This model is particularly precise in describing the observational equivalences between probabilistic functional programs. In this talk, we'll present the proof that the exponential modality is the free commutative comonad, giving a further mark of canonicity to the model.
 Oct. 23, 2017, 5:30 p.m.

Charles Grellois (LIS, AixMarseille)
 Oct. 23, 2017, 10:45 a.m.

Marie Kerjean (IRIF, Paris Diderot)
With Yoann Dabrowksi.
The study of Differential Linear Logic argues for models of Linear Logic where proofs are interpreted as smooth functions between vector spaces endowed with a topology. However, several difficulties appears in this context : it is not trivial to endow a tensor product with a good topology, nor to find a cartesian closed category of smooth maps, or to construct a starautonomous category of topological vector spaces. We argue that the construction of these models should be done from the "parr" perspective, by interpreting this connective as the wellknown epsilon product of Schwartz. We exhibit several smooth classical models of Linear Logic, and argue for a general setting for the construction of such models.
 Oct. 24, 2017, 3:20 p.m.

Olivier Laurent (LIP, ENS Lyon)
We revisit the syntactic relations between classical linear logic (LL) and intuitionistic linear logic (ILL). This includes a study of doublenegation translations from LL to ILL and a new conservativity result for LL over ILL. Applying these results to LL and tensor logic (the “positive” fragment of ILL) allows us to show how the “at most one positive formula” property of focused systems for LL can be seen as a particular case of the “at most one righthand side formula” property of intuitionistic systems.
 Oct. 23, 2017, noon

Damiano Mazza (LIPN, Paris Nord)
 Oct. 23, 2017, 10 a.m.

Michele Pagani (IRIF, Paris Diderot)
With Thomas Ehrhard and Christine Tasson.
We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpoenriched cartesian closed category. This category gives a denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We prove the soundness and adequacy of this model with respect to a callbyname operational semantics and give some examples of its denotations.
 Oct. 24, 2017, 11:30 a.m.

Luc Pellissier (LIPN, Paris Nord)
With Giulio Guerrieri and Lorenzo Tortora de Falco.
We investigate how to determine whether a set of differential proofnet are elements of the Taylor expansion of the same proofnet. We give a partial answer for boxconnected proofnets, a geometric criterion.
 Oct. 24, 2017, 2:45 p.m.

Paolo Pistone
In categorial semantics, formulas are interpreted as multivariant functors and proofs as dinatural (or, more precisely, extranatural) transformations between such functors. In this context the correct notion of universal quantification is not the usual one (intersection) but the notion of "end". From a prooftheoretic viewpoint, dinaturality and extranaturality correspond to permutative principles (i.e. the fact that closed proofs are invariant, modulo normalization, with respect to a class of permutations). However this fact, which holds at the propositional and firstorder level, fails for second order logic (i.e. System F), due to the fact that the rules of second order quantification do not correspond to the definition of an end. As a consequence, System F is not fully dinatural.
In order to explore a notion of proof invariant with respect to all permutations arising from dinaturality/extranaturality I will consider proofnets for two main reasons: first, proofnets were invented to obtain proofs invariant with respect to permutation of rules; second, cutelimination in proofnets closely corresponds to composition of dinatural/extranatural transformations (as it appears clearly in EilenbergMacLane coherence theorems for monoidal categories). I will introduce a new notion of proofnet for second order logic reflecting these categorial intuitions. Such proofnets will be shown to be invariant with respect to all permutations arising from dinaturality.
 Oct. 23, 2017, 4 p.m.

Alexis Saurin (IRIF)Talk: Linear logic with fixed points and infinitary proofs, from straight threads to bouncing threads
Infinitary and circular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is notably based on two fundamental properties of a proof system: cut elimination and focalization. In this talk, we consider the infinitary proof system μMALL∞ for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish μMALL∞ as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems. In the last part of the talk, we will discuss some ongoing work on relaxing the validity condition for infinitary proofs and therefore accepting more proofs. This is motivated by the fact that usual validity conditions only consider straight threads  progressing from conclusion to premise. While natural in the cutfree setting, it is quite restrictive in presence of cut. This is joint work with Baelde, Doumane and Jaber.
 Oct. 23, 2017, 3 p.m.

Lionel Vaux (I2M, AixMarseille)
We introduce a notion of reduction on resource vectors, i.e. infinite linear combinations of resource λterms. The latter form the multilinear fragment of the differential λcalculus introduced by Ehrhard and Regnier, and resource vectors are the target of the Taylor expansion of λterms. We show that the reduction of resource vectors contains the image, through Taylor expansion, of βreduction in the algebraic λcalculus, i.e. λcalculus extended with weighted sums. We moreover exhibit a class of algebraic λterms, having a normalizable Taylor expansion: this subsumes both arbitrary pure λterms, and normalizable algebraic λterms. We then show that Taylor expansion and normalization commute.
 Oct. 24, 2017, 12:20 p.m.