Schedule
Oct. 23, 2017
- 10:00 – 10:45
-
Damiano Mazza (LIPN, Paris Nord)
- 10:45 – 11:30
-
Charles Grellois (LIS, Aix-Marseille)
- 11:30 – 12:00
- Coffee break
- 12:00 – 13:00
-
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 double-negation 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 right-hand side formula” property of intuitionistic systems.
- 15:00 – 16:00
-
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 under-developed. 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 cut-free setting, it is quite restrictive in presence of cut. This is joint work with Baelde, Doumane and Jaber.
- 16:00 – 17:00
-
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 proof-theoretic 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 first-order 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 proof-nets for two main reasons: first, proof-nets were invented to obtain proofs invariant with respect to permutation of rules; second, cut-elimination in proof-nets closely corresponds to composition of dinatural/extranatural transformations (as it appears clearly in Eilenberg-MacLane coherence theorems for monoidal categories). I will introduce a new notion of proof-net for second order logic reflecting these categorial intuitions. Such proof-nets will be shown to be invariant with respect to all permutations arising from dinaturality.
- 17:00 – 17:30
- Coffee break
- 17:30 – 18:15
-
Raphaëlle Crubillé
Probabilistic coherence spaces yield a model of linear logic and lambda-calculus 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. 24, 2017
- 11:30 – 12:20
-
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 cpo-enriched 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 call-by-name operational semantics and give some examples of its denotations.
- 12:20 – 12:55
-
Lionel Vaux (I2M, Aix-Marseille)
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.
- 12:55 – 13:30
-
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 proof-nets (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.
- 14:45 – 15:20
-
Luc Pellissier (LIPN, Paris Nord)
With Giulio Guerrieri and Lorenzo Tortora de Falco.
We investigate how to determine whether a set of differential proof-net are elements of the Taylor expansion of the same proof-net. We give a partial answer for box-connected proof-nets, a geometric criterion.
- 15:20 – 15:55
-
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 star-autonomous 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 well-known 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.
- 16:00 – 19:00
- General meeting