Groupe de travail Sémantique

Le groupe de travail se réunit au 3e étage du bâtiment Sophie Germain le mardi de 11h à 12h15, en salle 3052.

LA NOUVELLE PAGE DU GDT SEMANTIQUE SE TROUVE ICI.

Exposés à venir

Mardi 29 mars 2016 à *10h30* (Attention: horaire inhabituel ! salle 3052)
Andrew Polonsky (IRIF)
TBA

Exposés passés

Mardi 22 mars 2016 à *10h30* (Attention: horaire inhabituel ! salle 3052)
Matteo Acclavio (I2M, Marseille)
String diagrams for Proof nets

Sequentialization of MELL proof nets needs additional tools extern to interaction nets syntax: connectivity, switchings, boxes and jumps. In this talk we introduce string diagrams syntax for monoidal categories in order to present a model for proof nets (with the relative cut elimination) with a unique local sequentialization criterion for MLL with constants and an idea for a generalization of this result for MELL proof nets.

Mardi 8 mars 2016 à 11h en salle 3052
Antonino Salibra (Univ. Ca' Foscari de Venise)
Factor Varieties and Symbolic Computation

Abstract: We propose an algebraization of classical and non-classical logics, based on factor varieties and decomposition operators. In particular, we provide a new method for determining whether a propositional formula is a tautology or a contradiction. This method can be automatized by defining a term rewriting system that enjoys confluence and strong normalization. This also suggests an original notion of logical gate and circuit, where propositional variables becomes logical gates and logical operations are implemented by substitution. Concerning formulas with quantifiers, we present a simple algorithm based on factor varieties for reducing first-order classical logic to equational logic. We achieve a completeness result for first-order classical logic without requiring any additional structure.

Mardi 12 janvier 2016 à 11h (salle 3052)
Daniel de Carvalho (Innopolis, RU)
Le modèle relationnel est injectif pour MELL

On montre que la sémantique relationnelle est injective pour le fragment multiplicatif exponentiel des réseaux de preuve de la logique linéaire, c'est-à-dire que l'égalité entre les réseaux de preuve de MELL dans le modèle relationnel est exactement axiomatisée par l'élimination des coupures.

Mardi 8 décembre 2015 à 11h (salle 3052)
Federico Aschieri (TU Wien)
Game Semantics and the Complexity of Interaction

In modern game semantics two research lines have run in parallel for quite a while, to such an extent they are often mistakenly considered different semantics. They are the logical tradition of Coquand and the computer science tradition of Hyland-Ong. It turns out that these two traditions combined together provide all the tools we need for a new, very refined complexity analysis of several computational phenomenons. We are speaking of: first-order cut-elimination, normalization, interaction between Herbrand expansion trees and any other dialogical process game semantics can model and apply to.

Of course, having all the pieces of a puzzle is not enough to guess the picture that they form: our contribution is precisely to rearrange the many pieces scattered on the table and to show what this picture is. In particular, we present abstract complexity results about Coquand-Hyland-Ong game semantics; we provide a novel method to bound the length of interactions between bounded visible strategies and to measure precisely the tower of exponentials defining the worst-case complexity. Our study improves the old estimates on average by several exponentials.

Mardi 24 novembre 2015 à 11h (salle 3052)
Matthieu Picantin (LIAFA)
Semi-groupes d’automate et semi-groupes automatiques

Comme leur nom l'indique, les (semi-)groupes d’automate et les (semi-)groupes automatiques sont définis à partir d’un même objet: un automate ou, plus précisément, un transducteur lettre-à-lettre. En dépit de cette origine commune, ces deux thématiques restaient essentiellement distantes depuis trente ans, que ce soit en terme de communauté ou en terme d’outils et de résultats. Nous établissons une possible connexion entre « être un semi-groupe automatique » et « être un semi-groupe d’automate »: tout semi-groupe simplifiable admettant un langage spécial de formes normales peut s’interpréter comme un semi-groupe d’automate, en l'occurrence le semi-groupe engendré par une machine de Mealy qui encode le comportement d’un tel langage de formes normales vis-à-vis de la multiplication. Nous verrons pourquoi cette connexion en fait des propriétés duales. Cette approche effective englobe l'essentiel des familles connues de semi-groupes automatiques: semi-groupes libres, semi-groupes libres commutatifs, monoïdes de traces et de Droste-Kuske, monoïdes de tresses, d’Artin-Tits ou de Krammer, semi-groupes de Baumslag-Solitar, etc. Comme les monoïdes plaxiques ou chinois, certains semi-groupes non-simplifiables sont également étudiés.

Mardi 17 novembre 2015 à 11h (salle 3052)
Andrew Polonsky (PPS)
The Y=Y(SI) problem

We discuss an important problem in untyped lambda calculus. Put forward by Statman, it asks whether there exists a fixed point combinator Y such that Y=Ydelta, where delta = SI = \yx.x(yx). It is conjectured that there is no such Y.

After basic introduction and examples, we will show how Statman's conjecture naturally generalizes in two directions.

In the first perspective, we investigate general conditions on terms G1,..,GN which are fpc generators: for all terms M, M fpc => M G1 .. GN fpc

In the second direction, we look at the simply-typed \Y-calculus, in which a "formal" fpc is introduced together with the rewrite rule Yx –> x(Yx) Given an arbitrary fpc Y, there is an obvious interpretation of this calculus in the untyped lambda calculus. The Y=Y(SI) conjecture is reduced to the conservativity of this interpretation, for any Y.

Mardi 3 novembre 2015 à 11h (salle 3052)
Paul-André Melliès (PPS)
Dialogue categories and Frobenius monoids

About ten years ago, Brian Day and Ross Street discovered a beautiful and unexpected connection between the notion of star-autonomous category in proof theory and the notion of Frobenius algebra in mathematical physics. In this talk, I will investigate the logical content of this connection by formulating a two-sided presentation of Frobenius algebras. The presentation is inspired by the idea that every logical dispute has two sides consisting of a Prover and of a Denier. This dialogical point of view leads us to a correspondence between tensorial logic, dialogue categories and a lax notion of Frobenius monoid. The correspondence refines Day and Streets original correspondence in the same way as tensorial logic (or equivalently dialogue games and innocent strategies) refines linear logic. I will explain at the end of the talk how to depict tensorial proofs in the graphical language of cobordism.

You will find here the slides of my talk recently given during a workshop in Vienna devoted to higher topological quantum field theory and categorical quantum mechanics: http://www.pps.univ-paris-diderot.fr/~mellies/slides/dialogue-categories-and-frobenius-monoids.pdf

Mardi 10 novembre 2015 à 11h (salle 3052)
Paul-André Melliès (PPS)
Dialogue categories and Frobenius monoids

Je n'ai pas pu finir mon exposé la semaine dernière et je le poursuivrai donc cette semaine en expliquant en détail les liens entre catégories de dialogue et algèbres de Frobenius.

Jeudi 15 octobre 2015 à 14h (salle 3052)
Daniela Petrisan (LIAFA-PPS)
Coinduction up-to in a fibrational setting

Bisimulation is used in concurrency theory as a proof method for establishing behavioural equivalence of processes. Up-to techniques can be seen as a means of optimizing proofs by coinduction. For example, to establish that two processes are equivalent one can exhibit a smaller relation, which is not a bisimulation, but rather a bisimulation up to a certain technique, say ‘up-to contextual closure’. However, the up-to technique at issue has to be sound, in the sense that any bisimulation up-to should be included in a bisimulation.

In this talk, I will present a general coalgebraic framework for proving the soundness of a wide range of up-to techniques for coinductive unary predicates, as well as for bisimulations. The specific up-to techniques are obtained using liftings of functors to appropriate categories of relations or predicates. In the case of bisimulations with silent moves the situation is more complex. Even for simple examples like CCS, the weak transition system gives rise to a lax bialgebra, rather than a bialgebra. In order to prove that up-to context is a sound technique we have to account for this laxness. The flexibility and modularity of our approach, due in part to using a fibrational setting, pays off: I will show how to obtain such results by changing the base category to preorders.

This is joint work with Filippo Bonchi, Damien Pous and Jurriaan Rot.

Jeudi 15 octobre 2015 à 15h (salle 3052)
Zoltan Esik (University of Szeged)
Solving fixed-point equations involving non-monotonic functions

Rondogiannis and Wadge (2005) gave a novel semantics to logic programs possibly involving negation using an infinite space of truth values. In the talk, I will develop the elements of an abstract fixed point theory based on their approach that seem to have several other potential applications.

Mardi 6 octobre 2015 à 11h
Fabio Pasquali (Marseille)
Free construction in triposes

We analyze some relevant free constructions which involve the notion of tripos.

In particular we focus on those constructions which add extensionality, comprehension, quotients and functional completeness to a given tripos. We show that the composition of these gives the tripos-to-topos construction. We comment on the connection between functional completeness and sheafification.

Mercredi 17 juin 2015 à 16h
Kenji Maillard (ENS)
A fibrational account of local stores

In preparation to my talk at LICS next month, I will give a short presentation (about thirty minutes) of a recent work in collaboration with Paul-André Melliès. I will more specifically explain how the local state monad introduced by Gordon Plotkin and John Power may be recovered by gluing together a family of global state monads. The gluing data is formulated as a 2-functor from a basis 2-category into a 2-category of monads formulated by Ross Street in the 1970s. An algebra of the local state monad iq then described as a section of a specific bundle of algebras of the global state monads. This alternative account of the local state monad provides a clean and modular understanding of local states.

Mardi 16 juin 2015 à 11h
Jim Laird (Bath University)
Quantitative Semantics for Mobility.

In previous work, Giulio Manzonetto, Guy McCusker, Michele Pagani and I described a "quantitative" denotational semantics. The basic idea is that given any continuous semiring R we can construct a model of linear type theory - and thus the lambda-calculus - in which programs correspond to matrices over R, and which is sound with respect to an operational semantics which evaluates non-deterministic programs by summing their weighted reduction-paths in R. This is nice because it's a simple model - "everyone knows what a matrix is" - and because it seems to represent interesting properties of computation — cost, probability, security level, shortest path, etc. - all of which are already studied using static networks weighted with values from semirings. But it raises further questions, both about the computation being modelled - non-deterministic functional programs match neither the problem domain nor the model particularly well (in formal terms, there's a failure of full abstraction) - and what can be measured - the continuity requirement on R makes some proofs easier but it's not clear that it is necessary.

I will develop this critique based on two claims: (a) that our model gives a natural interpretation of networks with "mobile topology" and (b) it can be constructed based on complete semirings which are not continuous, generating new examples. Specifically, I will describe: A type theory (unidirectionality) for name-passing mobility based on Laneve and Victor's solo calculus, which has minimal syntax, is able to express other formalisms like lambda and pi-calculi economically, and has a simple graphical representation via Ehrhard and Regnier's differential nets. For any complete semiring R, an operational semantics evaluating closed unidirectional solo terms as elements of R, and a corresponding fully abstract denotational semantics of unidirectional solo terms as matrices over R.

Mardi 2 juin 2015 à 11h
Gabriel Scherer (Gallium, INRIA Rocquencourt)
Consistent coercion calculi, and reduction in the face of absurdity

Consistent coercion calculi were recently (2010-2014) proposed by Julien Crétin and Didier Rémy as an expressive framework to easily compose and combine together various type-system features, notably subtyping and polymorphism. Contrarily to most "all-encompassing type system frameworks" out there, they enforce a very clear separation between the program text, specifying the dynamic semantics, and the type information present in derivations that does not influence the program execution. They are also defined for full reduction, which makes them sound for any reduction strategy (not just one of strict or lazy evaluation).

In later work (2015) with Didier Rémy, I extended consistent coercion calculi with a form of "inconsistent abstraction" that allows to abstract over logical assumptions that might be incorrect. To preserve soundness, we have to block reduction around these assumptions, resulting in a mix of full and weak reduction. This is necessary to express some modern programming features, such as GADTs. There is then a surprising coincidence, with a feature ("hiding") motivated by programming language design that turns to be essential to get good meta-theoretical properties (confluence).

Mardi 19 mai 2015 à 11h
Andrew Polonsky (PPS et LIPN)
A Coinductive Framework for Infinitary Rewriting

We present a coinductive approach to infinitary rewriting. Whereas the classical approach is based on ordinal-indexed sequences of rewrite steps, the new approach defines the binary relation ->>> between infinite terms directly by coinduction. For instance, the infinitary rewriting relation between lambda terms may be defined thus

M ->> M1 M2 M1 ->>> N1 M2 ->>> N2
————————————————–
M ->>> N1 N2

M ->> \x. M' M' ->>> N'
—————————–
M ->>> \x. N'

M ->> x
———-
M ->>> x

Here ->> denotes the inductive finite-step reduction between infinite terms, and ->>> the infinitary reduction relation. The double lines signify that the inference rules are to be understood coinductively, as defining a maximal fixed point of a monotone map on the powerset of /\^oo x /\^oo.

With this definition, it becomes straightforward to formalize the theory of infinitary rewriting in proof assistants using coinductive types. As a test case, we formalized in Coq infinitary compression and standardization. The formalizations are completely constructive, and the Coq code actually computes the infinite standardisations.

Mardi 12 mai 2015 à 11h
Lionel Vaux (Université de Aix-Marseille)

A characterization of strong normalizability by a finiteness structure via the Taylor expansion of λ-terms

In the folklore of differential linear logic and its denotational models, a common intuition is that the structure of finiteness spaces, introduced by Ehrhard, semantically reflects the strong normalization property of cut-elimination.

We make this intuition formal in the context of λ-calculus by introducing a finiteness structure on resource λ-terms, which is such that a λ-term is strongly normalizing iff the support of its Taylor expansion is finitary.

This structure is a refinement of the one introduced by Ehrhard in his LICS 2010 paper: for the latter, we also prove that any strongly normalizing λ-term has a finitary Taylor expansion (this was already known for the terms of system F), but the converse does not hold. As was already the case in Ehrhard's work, the proofs do not rely on any uniformity property, hence this approach is valid for non-deterministic extensions of the λ-calculus as well.

One application of this work is then the existence of a normal form for the Taylor expansion of any strongly normalizable term. This is a necessary first step to extend previous results of Ehrhard and Regnier (TCS 2008) that were limited to a uniform setting.

(joint work with Michele Pagani and Christine Tasson)

Mardi 31 mars 2015 à 11h
Frédéric Gava (Université de Paris Est)
Sémantiques opérationnelles en Coq d'un mini-langage impératif BSP doté de la sous-synchronisation

Le modèle de parallélisme quasi-synchrone BSP est un modèle structuré de parallélisme qui permet la portabilité des programmes tout en offrant une prévision réaliste de leurs performances sur une grande variété d'architectures. Nous présentons un mini-langage impératif pour la preuve d'algorithmes BSP avec sous-synchronisation ainsi que des sémantiques opérationnelles dans l'assistant de preuve Coq. Nous donnerons quelques lemmes et des cas d'utilisation dans le cadre de la vérification déductive d'algorithmes BSP de model-checking.

Mardi 24 mars 2015 à 11h

Raphaelle Crubille (Università di Bologna / Université de Paris Diderot)
Metric reasoning about lambda-terms : the affine case

Terms of Church's lambda-calculus can be considered equivalent along many different definitions, but context equivalence is certainly the most direct and universally accepted one. If the underlying calculus becomes probabilistic, however, equivalence is too discriminating: terms which have totally unrelated behaviours are treated the same as terms which behave very similarly. We study the problem of evaluating the distance between affine lambda-terms. The most natural definition for it, namely a natural generalisation of context equivalence, is characterised by a notion of trace distance, an bounded from above by a coinductively defined distance based on the Kantorovich metric on distributions. A different, again fully-abstract, tuple-based notion of trace distance is able to handle nontrivial examples.

Mardi 10 et 24 février 2015 à 11h
Thierry Coquand (University of Gothenburg)
Theorie des types et axiome d'univalente.

Abstract: Le but de ces exposes sera de présenter un modèle de la théorie des types dans les ensembles cubiques. Ce modèle justifie de manière effective l'axiome d'univalence et les nouveaux types inductifs supérieurs (cercle, suspensions, push-out,…) Le premier exposé sera une introduction générale au problème avec une présentation de l'axiome d'univalence (qui exprime la loi d'extensionalite en théorie des types dépendants) et l'idée qu'un type doit être représenté par un type d'homotopie. La question est alors de trouver une formulation "combinatoire" de la notion de type d'homologie, question qui sera discutée dans le deuxième expose.

Transparents séance 1: ici.

Mardi 13 janvier 2014 à 16h
Luc Pellissier (LIPN)
Une autre formule explicite pour l’exponentielle libre en logique linéaire.

Melliès, Tabareau et Tasson ont introduit en 2009 une formule permettant de calculer le comonoïde co-commutatif libre sous n’importe quel objet d’une catégorie symétrique monoïdale avec produits (c’est-à-dire le modèle libre de LL à partir d’un modèle de MALL) vérifiant certaines propriétés supplémentaires, vérifiées dans différents modèles usuels de la logique linéaire. Mazza a, à partir de 2013, développé un lambda-calcul affine infinitaire dont le lambda-calcul classique est un quotient et permettant notamment d’exprimer des résultats de complexité. On se propose (en commun avec Damiano Mazza) de connecter ces travaux via une approche sémantique du lambda-calcul affine infinitive.

Lundi 29 septembre 2014 à 16h
Bas Spitters
Formalizing mathematics in the univalent foundations.

We have been formalizing mathematics in type theory for many years. Although great progress has been made, there were still a number of issues that were hard to tackle, especially when leaving the realm of discrete mathematics. We mention a lack of quotient types and the absence of a clear mathematical semantics for the Coq type theory.

Homotopy type theory promises a solution to these challenges. I will discuss how to develop some mathematics in the univalent foundations and report on the design of our Coq library.

Basic familiarity with type theory and some categorical semantics is assumed.

Mercredi 1er octobre 2014 à 14h (en salle 1007)
Stefan Milius (FAU Erlangen-Nürnberg)
Uniform Eilenberg Theorem: Syntactic Algebras For Free

We investigate the duality between algebraic and coalgebraic recognition of languages to derive a generalization of Eilenberg’s theorem. The classical Eilenberg theorem states that the lattice of all boolean algebras of regular languages closed under derivatives and preimages of homomorphisms is isomorphic to the lattice of all pseudovarieties monoids. By applying our method to different categories, we obtain several previously known and also new Eilenberg-type theorems as special instances. And we also have uniform proofs for local versions of Eilenberg-type theorems, e.g. one due to Gehrke, Grigorieff and Pin, weakens boolean algebras to distributive lattices, one due to Polák weakens them to join-semilattices, and the last one considers vector spaces over Z_2.

Mardi 7 octobre 2014
Giulio Guerrieri (PPS)
Injectivity of relational semantics for connected MELL proof-structures via Taylor expansion

We show that: (1) the Taylor expansion of a cut-free MELL proof-structure R with atomic axioms is the (most informative part of the) relational semantics of R; (2) every connected MELL proof-structure is uniquely determined by the element of order 2 of its Taylor expansion; (3) the relational semantics is injective for connected MELL proof-structures. Our results are deeply related to a previous work of Lorenzo Tortora de Falco and Daniel de Carvalho, but is based on a slightly different viewpoint.

Mardi 21 octobre 2014
Relâche pour cause de soutenance de thèse

Mardi 18 novembre 2014
Relâche pour cause de réunion ANR

Mardi 1er avril 2014
Timothy Bourke (INRIA and ENS)
Zélus: a synchronous language with Ordinary Differential Equations

Tools for modeling hybrid systems—like Modelica, LabView, and Simulink/Stateflow—are rightly understood and studied as programming

languages. Indeed, models are now used not only for simulation, but also for test-case generation, formal verification, and translation to embedded code. Important underlying issues include defining rules for composing discrete and continuous elements, analyzing the causality of communications between those elements, and providing efficient, and eventually certifiable, compilation to sequential code either for direct execution on an embedded platform or for simulation by numerical approximation.

In this talk, I will show that these issues challenge even such high-quality and widely-used tools as Simulink/Stateflow, and present a language called Zélus that we are developing to understand and address them. The main originality of Zélus, from a user's perspective, is to extend an existing Lustre-like synchronous language with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as data-flow equations and hierarchical automata can be composed arbitrarily with ODEs in the same source code. The underlying mathematical model is the synchronous parallel composition of stream equations, ODEs, and imperative features.

Zélus shows that it is possible to build a modeler for explicit hybrid systems using an existing synchronous language as both a semantic basis and a target for code generation. A dedicated type system and causality analysis ensure that all discrete changes are aligned with zero-crossing events so that no side effects or discontinuities occur during integration. Programs are statically scheduled and translated into sequential code that, by construction, runs in bounded time and space. Compilation is effected by source-to-source translation into a small synchronous subset which is processed by a standard synchronous compiler architecture.

In collaboration with: Albert Benveniste (Inria) Benoit Caillaud (Inria) Marc Pouzet (UPMC, ENS, and Inria)

Mardi 11 mars 2014
Flavien Breuvart (PPS)
Un pont entre les semi-anneaux.

Il s'agirait d'une mise à jour de l'exposé que j'ai fait à Fontainebleau en décembre et que je vais présenter à Birmingham et Dundee dans quelques semaines. Ces 25 dernières années ont vu la naissance de plusieurs langages typés qui à l'instar de BLL (Girard1987)

utilisent un découpage fin de l'exponentiel pour imposer ou exhiber des garantis fines sur les ressources (au sens large) utilisées. Plus récemment deux articles (GhicaSmith2013, BrunelGaboardiMazzaZdancewic2013) tentent de généraliser ces construction (d'abord sous une forme non dépendante) en permettant l'utilisation d'un semi-anneau ordonné pour définir ces typages. Le but de cet exposé sera d'étudier la sémantique (catégoriques et concrètes) de ces langages et la signification des ces semi-anneaux.

A bridge between semirings.

This talk will be an update of the presentation I gave at Fontainebleau on December that I will present at Birmingham the week after. This 25 last years have seen many typed languages that, like BLL (Girard1987), use an nontrivial decomposition of LL exponential in order to impose or exhibit warranties on used resources. More recently, tow articles (GhicaSmith2013, BrunelGaboardiMazzaZdancewic2013) did generalized this constructions (firstly only non dependent ones) by using an ordered semiring pour to design this typing systems. The goal of this talk will be to study the semantic (both categorical and concrete) of this languages and the significations of this semi rings.

Mardi 11 février 2014 à 11h
Baptiste Mélès (Université de Clermont-Ferrand)
Approche philologique des langages de programmation

La théorie des langages de programmation s'appuie généralement sur des langages de programmation théoriques — lambda-calcul, machines de Turing, et leurs variantes — que l'on suppose représenter fidèlement — à

compilation près ! — les propriétés des langages de programmation de la « vraie vie », si l'on entend par là ceux que les programmeurs utilisent pour écrire des programmes utiles au quotidien : C, C++, Perl, etc.

Or nous allons voir que les langages de programmation de la vraie vie possèdent bien des propriétés dont nul ne voudrait dans un langage théorique, et que la compilation écrase : des commandes inutiles, des redondances, des résidus purement historiques... Qui plus est, loin d'être un fait simplement négatif, ces propriétés constituent une bonne part de leur expressivité du point de vue du programmeur, et sont autant de points communs avec les langues naturelles. Nous verrons ainsi que des outils linguistiques et philologiques peuvent être mobilisés pour décrire une « sémantique du programmeur », qui échappe pour une bonne

part aussi bien aux sémantiques courantes des langages de programmation qu'aux tentatives de description formelle de l'expressivité des langages de programmation.

Mardi 4 février à 11h
Elaine Pimentel (Université de Rio Grande do Norte)
Relating Focused Proofs with Different Polarity Assignments (joint work with Vivek Nigam)

This is a *very informal* talk on some ongoing work, where we will reason on how a given focused proof where atoms are assigned with some polarity can be transformed into another focused proof where the polarity assignment to atoms is changed. More specifically, using the intuitionistic focused system LJF

restricted to Harrop formulas, we define a procedure, introducing cuts, for transforming a focused proof, where an atom is assigned with positive polarity, into another focused proof, where the same atom is assigned negative polarity and vice-versa. Then we show how to eliminate these cuts, obtaining the not at all surprising, but yet interesting result: while the process of eliminating a cut on a positive atom gives rise to a proof with one smaller cut, in the negative case the number of introduced cuts grows exponentially. This difference in the cut-elimination algorithm is, of course, related to the different evaluation strategies according to the Curry-Howard isomorphism, where cut-elimination corresponds to computation in a functional programming setting. Hence we can propose a single calculus which incorporates both evaluation strategies cbn and cbv.

Mercredi 22 janvier à 14h
Cécilia Flori (Perimeter Institute)
Compositories and Gleaves

Sheaves are objects of a local nature: a global section is determined by how it looks like locally. Hence, a sheaf cannot describe mathematical structures which contain global or nonlocal geometric information. We introduce the notion of gleaf as a presheaf together with a certain additional piece of data. In contrast to sheaves, gleaves can describe geometric structure of a global nature. The prototypical example is the gleaf of (pseudo-)metrics over a set: assigning to every subset the collection of pseudometrics on that subset is a presheaf which turns out to be a gleaf in a natural way. Moreover, we describe a related notion of higher category called compository. A compository is a simplicial set in which an m-simplex and an n-simplex can be composed along a common k-simplex, and the composition is an (m + n - k)-simplex. There is a multitude of examples of such structures: nerves of categories, compositories of higher spans in categories, compositories constructed in terms of gleaves, and compositories of joint probability distributions of random variables.

The material of this talk is based on the following paper: http://arxiv.org/abs/1308.6548

Mardi 14 janvier
Relâche en raison des journées Mathematical Structures of Computation à Lyon.

Mardi 7 janvier à 11h
Thomas Seiller (INRIA-IHES)
Autour de l'équation de rétroaction

Dans le cadre de son programme de Géométrie de l'Interaction, Girard a introduit l'équation de rétroaction, qui traduit la coupure entre deux (interprétations de) preuves. Résoudre cette équation revient donc à calculer (l'interprétation de) la forme normale d'une preuve. J'expliquerai dans un premier temps d'où vient cette équation, puis expliquerai les cas où celle-ci peut être résolue. Je montrerai ensuite comment les solutions de cette équation sont reliées au déterminant, faisant apparaitre naturellement une adjonction. Finalement, je donnerai une interprétation combinatoire de la solution de l'équation de rétroaction, du déterminant, et de l'adjonction qui les relie.

Mardi 12 novembre à 11h
Thomas Powell (IHES)
Bar recursive extensions of Goedel's system T

Extensions of Goedel's system T with variants of bar recursion play a crucial role in proof theory, where they are used to give a computational interpretation to strong subsystems of mathematics based on the axiom of countable choice. The canonical example of this is Spector's bar recursion, devised in the 1960s to solve the Dialectica interpretation of the double negation shift. However, the last decade or so has seen the development of a much broader variety of such extensions, including modified bar recursion, the symmetric `demand-driven' functional of Berardi, Bezem and Coquand, the update and open recursors of Berger and more recently the products of selection functions of Escardo and Oliva. In this talk I discuss aspects of the computability theory of bar recursion and its variants, and in particular I give an account of recent work on establishing the relationship between these variants and classifying extensions of system T according to their computational strength.

Mardi 22 octobre à 11h
Pierre-Marie Pédrot (PPS)
Dialectica peut-elle casser des briques ?

La transformation fonctionnelle de Gödel, aussi appelée « Dialectica », du nom de la revue où Gödel la présenta en 1958, est à l'origine une traduction de HA dans HAω, motivée par l'expressibilité intuitionniste d'axiomes semi-classiques qui fleure bon la protohistoire de la théorie de la démonstration. En nous appuyant sur une reformulation basée sur la logique linéaire, due à de Paiva, nous en donnerons une présentation compatible avec les standards actuels de la théorie de la démonstration. En particulier, nous verrons que le contenu calculatoire de cette interprétation est relativement simple, surtout vu au travers des machines abstraites, et résolument incorrect, surtout vu au travers des machines abstraites. Une adaptation directe de cette présentation nous permettra d'appliquer Dialectica à des systèmes logiques plus complexes, comme le calcul des constructions par exemple.

Mardi 8 octobre 2013 à 11h
Paul-André Melliès (PPS)
Jeux de dialogue et séquentialité

Dans cet exposé, j'expliquerai comment opérer une synthèse harmonieuse entre structures de données concrètes au sens de Berry et Curien et jeux d'arènes au sens de Hyland et Ong. Cette synthèse des deux paradigmes historiques de la sémantique des jeux permet d'identifier la catégorie de dialogue libre avec sommes comme une catégorie de jeux de dialogue et de stratégies innocentes. Vue sous cet angle, la sémantique des jeux apparait comme une syntaxe des continuations linéaires, que l'on s'amusera à interpréter dans différents modèles de la logique tensorielle: espaces de cohérence, bistructures, etc.

Mardi 1er octobre 2013 à 11h
Thomas Ehrhard (PPS)
Collapse extensionnel du modèle relationnel du lambda-calcul

La catégorie des ensembles et des relations fournit un modèle simple et naturel du lambda-calcul et de la logique linéaire, et en particulier une CCC contenant des objets réflexifs. Ce modèle est quantitatif: il tient compte des multiplicités dans les calculs et la CCC associée n'est pas extensionnelle. On verra que son collapse extensionnel est une CCC de treillis complets et de fonction Scott continues qui est une sémantique purement "qualitative". On interprètera ce résultat en termes de systèmes de types avec intersections (idempotentes / non idempotentes).

Exposés passés (2012-2013)

Jeudi 4 juillet 2013 à 11h
Matthieu Anel (ETH Zürich)
Enrichissement des algèbres sur les cogèbres

C'est un travail en collaboration avec André Joyal. Le résultat fondamental est que la catégorie des dg-coalgèbres est monoïdale fermée et que la catégorie des dg-algèbre est enrichie, bicomplète et monoïdale sur celle des dg-coalgèbres. Cette structure produit six opérations sur les algèbres et coalgèbres qui peuvent être utilisées pour construire plusieurs type d'adjonctions entre les catégories d'algèbres et de coalgèbres. Nous retrouvons ainsi nombre d'adjonctions déjà connues (algèbres de jets, dualité algèbre-cogèbre, adjonction bar-cobar)

Lundi 24 juin 2013 à 14h
André Joyal (UQAM)
Aspects catégoriels de la théorie homotopique des types

Il s'agira dans cet exposé de décrire la théorie des types de Martin-Lof en termes purement catégoriels.

Mardi 25 juin à 11h
Robin Cockett (University of Calgary)
Abstract computability: unifying complexity and computability

A benefit of abstract computability – which is the main subject matter of this talk – is that it allows the explicit unification of complexity and computability. Understanding the broader geography of these subjects is important for a number of reasons: it brings new perspectives to an old subject and it allows new tools to be brought to bear on old problems.

Abstract computability defines {\em what\/} one is modelling but is very flexible both on the {\em how\/} and the {\em where\/}. Of particular significance in this talk is the issue of {\em where\/} one models computability – this flexibility adds a new dimension to computability. The talk demonstrates how complexity can be viewed as computability in the ``timed sets''. Significantly, this mimics precisely what complexity theorists actually do. The abstract approach, however, has the advantage of removing conceptual clutter and clarifying the structure of what is happening.

Abstract computability is based round the notion of a Turing category: the talk will introduce this and the necessary related structures.

References:
Robin Cockett, Joaquin Diaz-Boïls, Jonathan Gallagher, Pavel Hrubes ``Timed Sets, Functional Complexity, and Computability'' {\em Electronic Notes in Theoretical Computer Science Volume 286, 24 September 2012, Pages 117–137.}
Robin Cockett, Pieter Hofstra ``Introduction to Turing Categories'' {\em Annals of Pure and Applied Logic, Volume 156, Issues 2–3, December 2008, Pages 183–-209}

Mercredi 19 juin à 14h
John Bourke (Macquarie University)
Weak natural factorisation systems in 2-categories

Mardi 11 juin à 10h
Guilhem Jaber
Proving Equivalence of Programs using Kripke Logical Relations and Temporal Logic
(Joint work with Nicolas Tabareau)

To deal with contextual equivalence for higher-order functional languages with local states, Pitts and Stark have introduced Kripke Logical Relations, with a notion of world which represents invariants on heaps. This model was refined by Dreyer, Neis and Birkedal, so that worlds can represent evolutions of invariants, using State Transition Systems. Their model is complete thanks to the use of biorthogonality, but in practise only direct-style proofs can be used (as shown with the so-called “awkward example” in the work of Pitts and Stark).

In this talk, we will present a complete direct-style definition of Kripke Logical Relations, refining their model by taking care of disclosure of names between a term and its context. We will take advantage of this direct definition to construct a temporal logic to reason on worlds as STS. This temporal logic will be used to generate automatically, for any two programs, a formula which is true if and only if the two programs are contextually equivalent. We then discuss how to prove such formulas automatically in some particular cases.

We finally compare our approach to recent work on Algorithmic Game Semantics by Hopkins, Murawski, Ong and Tzevelekos.

Mardi 11 juin à 11h15
Camille Male (LPMA)
Une utilisation des opérades en probabilités libres et matrices aléatoires.

Motivé par l'étude des algèbres de von Neumann, Voiculescu introduit dans les années 80 les espaces de probabilités non commutatives et leur produit libre. Ces espaces sont les *-algèbres unitaires munies d'une forme linéaire, unitaire, traciale et positive qui joue le rôle de l'espérance. Le produit libre replace dans ce contexte l'indépendance statistique. Quelques années plus tard, Voiculescu établit une connexion entre les probabilités libres et les grandes matrices aléatoires. Des familles de matrices aléatoires indépendantes et invariantes en loi par conjugaison par des matrices unitaires sont asymptotiquement libres lorsque leur taille tend vers l'infini. L'objectif de cet exposé introductif est de montrer comment les opérades permettent de définir de nouveaux espaces de probabilités non commutatives (dont la *-algèbre est une algèbre sur une opérade de graphes). Dans ce contexte, on sait résoudre des questions de matrices aléatoires plus générales que celles abordées par Voiculescu, en particulier l'étude des familles de matrices aléatoires indépendantes et invariantes en loi par conjugaison par des matrices de permutation.

Mardi 4 juin à 10h
Marie Kerjean (PPS)
Complete vector space, a denotational model of DiLL ?

Convenient spaces were first introduced 25 years ago by Frölicher and Kriegl as dualized vector spaces, or as Mackey-complete bornological locally convex vector spaces with slightly different smooth maps on them. In 2010, R. Blute, T. Ehrhard and C. Tasson saw in them a model of intuitionisitic linear logic, as well as a differential category.

In fact, even if bornological structures are meaningful in this setting, they are not necessary. Furthermore, we can simplify the Mackey-completeness condition by strenghtening it in a simple completeness condition: complete lcs, with smooth maps as co-Kleisli maps, is a Seely category, supplied with derivative and co-derivative.

While looking for a good Taylor formula, we can show that these results work also with real-analytic, holomorphic or even formal power series instead of smooth maps. The need for reflexive spaces can lead us to see our complete vector spaces as a generalization of Girard's Coherence Banach spaces, and as a model of differential linear logic.

Mardi 4 juin à 11h15
Chuck Liang (Hofstra University) & Dale Miller (INRIA-Saclay)
Unifying Classical and Intuitionistic Logics for Computational Control

We show that control operators and other extensions of the Curry-Howard isomorphism can be achieved without collapsing all of intuitionistic logic into classical logic. For this purpose we introduce a unified propositional logic using polarized formulas. We define a Kripke semantics for this logic. Our proof system extends an intuitionistic system that already allows multiple conclusions. This arrangement reveals a greater range of computational possibilities, including a form of dynamic scoping. We demonstrate the utility of

this logic by showing how it can improve the formulation of exception handling in programming languages, including the ability to distinguish between different kinds of exceptions and constraining when an exception can be thrown, thus providing more refined control over computation compared to classical logic. We also describe some significant fragments of this logic and discuss its extension to second-order logic.

Mardi 4 juin à 16h30
Damiano Mazza (LIPN)
Non-Linearity as the Metric Completion of Linearity

We summarize some recent results showing how the lambda-calculus may be obtained by considering the metric completion (with respect to a suitable notion of distance) of a space of affine lambda-terms, i.e., lambda-terms in which abstractions bind variables appearing at most once. This formalizes the intuitive idea that multiplicative additive linear logic is ``dense'' in full linear logic (in fact, a proof-theoretic version of the above-mentioned construction is also possible). We argue that thinking of non-linearity as the ``limit'' of linearity gives an interesting point of view on well-known properties of the lambda-calculus and its relationship to computational complexity (through lambda-calculi whose normalization is time-bounded).

Mardi 21 mai 2013 à 10h30
Jacques van de Wiele
Théorie de la démonstration et invariants de noeuds de Vassiliev

Mardi 30 avril 2013 à 14h
Michael Emmi (LIAFA)
Analysis of Recursively Parallel Programs

We propose a general formal model of isolated hierarchical parallel computations, and identify several fragments to match the concurrency constructs present in real-world programming languages such as Cilk and X10. By associating fundamental formal models (vector addition systems with recursive transitions) to each fragment, we provide a common platform for exposing the relative difficulties of algorithmic reasoning. For each case we measure the complexity of deciding state-reachability for finite-data recursive programs, and propose algorithms for the decidable cases. The complexities which include PTIME, NP, EXPSPACE, and 2EXPTIME contrast with undecidable state-reachability for recursive multi-threaded programs.

Mardi 16 avril Matinée quantique – séance double

Premier exposé de la matinée à 10h
Alejandro Diaz-Caro (INRIA, Université Nanterre)
Vectorial types, non-determinism and probabilistic systems: towards a computational quantum logic.

We have the long-term goal of finding a computational quantum logic, in the sense of the proof-as-programs paradigm. That is, we want a logic such that its proofs are quantum programs. With this aim, we study several extensions of lambda-calculus highlighting different aspects such as superposition of programs, no-cloning, and non-deterministic and probabilistic projections.

11h Pause café

Second exposé de la matinée à 11h15
Rui Soares Barbosa (University of Oxford)
Structural reason for monogamy relations (and local realism of some macroscopic correlations)

We consider monogamy relations for violation of Bell-type inequalities, and their connection to a weak locality condition on correlations emerging in macroscopic quantum systems. We work within the sheaf-theoretic framework of Abramsky and Brandenburger [1], which provides a unified treatment of non-locality and contextuality in the general setting of no-signalling empirical models. General measurement scenarios are represented by simplicial complexes that capture the notion of compatibility of measurements, whereas non-locality and contextuality are realised as obstructions to the existence of global sections of a certain presheaf.

Monogamy and locality/noncontextuality of certain macroscopic correlations are revealed by our analysis as two sides of the same coin: correlations on the expectation values of macroscopic measurements are obtained by averaging along a symmetry (group action) on the microscopic measurements, while monogamy relations are exactly the inequalities that are invariant with respect to that symmetry. Our results exhibit a structural reason for monogamy relations and consequently for this weak form of macroscopic locality in the case of multipartite Bell-type scenarios. This sheds light on and also generalises the results in [2,3]. More specifically, we show that, however entangled the microscopic state of the system, and provided the number of particles in each site is large enough with respect to the number of allowed measurements, the macroscopic correlations of the kind considered are local realistic. The result relates to a classical mathematical result by Vorob’ev and depends only on the compatibility structure of the measurements, hence it applies generally to any no-signalling empirical model. Therefore, from another point of view, it can be read as a derivation of general multipartite monogamy relations from the no-signalling condition alone.

The generality of our scheme suggests a number of promising directions. In particular, they can be applied in more general scenarios to yield monogamy relations for contextuality inequalities and to study macroscopic non-contextuality.

[1] Samson Abramsky and Adam Brandenburger, “The sheaf-theoretic structure of non-locality and contextuality”, New J. Phys. 13, 113036 (2011). [2] Marcin Pawłowski and Časlav Brukner, “Monogamy of Bell’s Inequality Violations in Nonsignaling Theories”, Phys. Rev. Lett. 102, 030403 (2009). [3] R. Ramanathan, T. Paterek, A. Kay, P. Kurzyński, and D. Kaszlikowski, “Local Realism of Macroscopic Correlations”, Phys. Rev. Lett. 107, 060405 (2011). [4] N. N. Vorob’ev, “Consistent Families of Measures and Their Extensions”, Theory Probab. Appl. 7, 147 (1962), (translated by N. Greenleaf, Russian original published in Teoriya Veroyatnostei i ee Primeneniya).

Mardi 4 décembre 2012
Alice Jacquot (LIPN)
Une bijection entre lambda-termes linéaires et cartes combinatoires

Dans la suite de l'exposé d'Olivier Bodini sur l'énumération des lambda-termes, mais de manière tout à fait indépendante, Alice Jacquot nous donnera un exposé qui portera sur (1) une bijection entre les lambda-termes et les cartes combinatoires. et (2) une introduction à la génération aléatoire sous modèle de Boltzmann.

Mardi 20 novembre 2012
Olivier Bodini (LIPN)
Sur l'énumération des lambda-termes.

Nous présenterons dans cet exposé quelques résultats récents que nous avons obtenus en collaboration avec D. Gardy, A. Jacquot et B. Gittenberger sur l'énumération des lambda-termes. Notre approche repose sur la méthode symbolique et la combinatoire analytique. cet exposé sera adapté à un public non spécialiste de ces domaines.

Ieke Moerdijk (Radboud University, Nijmegen)

Série de cinq cours doctoraux sur la topologie dendroidale

Vendredi 26 octobre (10h à 12h en 0D07) — Dendroidal topology I — Manuscript of the first lecture.

Mardi 6 novembre (10h à 12h en 7D01) – Dendroidal topology II — Manuscript of the second lecture.
Mercredi 7 novembre (10h à 12h en 7D01) — Dendroidal topology III — Manuscript of the third lecture.
Mardi 13 novembre (10h à 12h en 7D01) — Dendroidal topology IV — Manuscript of the fourth lecture.
Mercredi 14 novembre (10h à 12h en 7D01) – Dendroidal topology V — Manuscript of the fifth lecture.

Dendroidal topology

Content: Dendroidal topology is an extension of simplicial topology, geared towards the theory of operads and of infinity-operads. In the first part of the course, we will discuss topological operads and their algebras, and the Boardman-Vogt resolution. Next, we will introduce the category of dendroidal sets, and the corresponding notion of infinity operad. This will naturally include a discussion of the Joyal model structure on simplicial sets and the corresponding notion of infinity category. The latter will automatically lead to a discussion of the Lurie theory of infinity operads. The course will end with a comparison between the Lurie model and the dendroidal model for infinity operads.

Prerequisites: The first two lectures should be accessible to anybody with basic knowledge of algebra, topology and category theory. The second part of the course will be hard to follow without familiarity with simplicial sets and some acquaintance with the notion of Quillen model category.

Mardi 23 octobre 2012
Gergei Bana (MSR-INRIA)
Towards Unconditional Soundness: Computationally Complete Symbolic Attacker

Traditionally, computational soundness of symbolic analysis of cryptographic protocols has meant defining a so-called Dolev-Yao symbolic model listing all possible moves of a symbolic adversary, and then showing that under certain circumstances, if there is no successful symbolic adversary to a protocol, then there is no successful computational adversary to the protocol either. However, "under certain circumstances" has always meant unreasonable restrictions on the computational implementation. In order to avoid such unreasonable restrictions, we choose a different approach to the symbolic adversary: instead of listing all possible moves, we only list some properties that the symbolic adversary is not allowed to violate, otherwise it is allowed to make any moves that are consistent with these properties. The properties are computationally valid, that is, computational adversaries must obey them. Such "permissive" symbolic adversaries can do everything that a computational adversary can, and therefore if there is no such successful symbolic adversary, there is no computational either without any further restriction. This soundness theorem turns out to be a natural application of Melvin Fitting's embedding of classical logic into S4.

Mardi 9 octobre 2012: Matinée thématique – Sémantique et complexité au LIPN

10h – 11h : Alois Brunel (LIPN)
Indexed realizability for bounded-time programming with references and type fixpoints
(Joint work with Antoine Madet)

The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging to a certain complexity

class. We here present a realizability semantics for a higher-order functional language based on a fragment of linear logic called LAL which characterizes the complexity class PTIME. This language also features recursive types and higher-order store. Our semantics involves biorthogonality, step-indexing and is quantitative, in the sense that it is able to keep track of the quantity of resources used by a program. This last feature enables us not only to derive a semantical proof of termination, but also to give bounds on the number of computational steps needed by typed programs to terminate.

11h – 11h15 : Pause Café

11h15 – 12h15 : Clément Aubert (LIPN)
Characterizing co-NL by a Group Action

In a recent paper, Normativity in Logic (2011), Girard uses the geometry of interaction in the hyperfinite factor in an innovative way to characterize complexity classes. As this paper is quite technical and sometimes allusive, we proposed with Thomas Seiller (Lama - Université de Savoie) a new presentation of its results. This talk will present the mathematical device that characterizes co-NL, a crossed product of the hyperfinite factor II_1 with the group of finite permutations, and the non-deterministic pointer machine, an abstract devices that computes the algorithms represented in this setting.

Mardi 2 octobre 2012
Alexis Goyet (PPS)
A dual calculus for non-innocent games.

The aim of the lambda lambda-bar calculus is to represent as faithfully as possible the structure of non-deterministic, non-innocent strategies in game semantics. Non-innocent strategies have been shown to model functional languages extended with references. The typical approach is to model the purely functional fragment with innocent strategies, to which a "memory-cell" strategy is added. Instead, our starting point is a simple concrete syntax of finite strategies, which are inherently non-innocent.

The resulting language is a dualization of the lambda calculus. A new binder, the lambda-bar, names arguments which have been passed to the environment (whereas the lambda names arguments which have been received). This makes explicit the act of answering a function call, and allows this answer to change over time, granting the power of effects.

Mardi 18 septembre 2012
Guillaume Scerri (LSV)
Reconciling two views of cryptography* : soundness theorems

Two main classes models exist for proving cryptographic protocols, the computational models close to real life cryptography and the symbolic models more abstract but more convenient for doing proofs. Since the seminal work of M. Abadi and P. Rogaway ("Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)" published in 2000) a lot of work have been done to understand the relationship between these two models. The main goal of this approach is to understand under which hypotheses a security proof in a symbolic model implies the security in a computational model. In this talk we will introduce these two models, explain their main differences and their relationship, reviewing some soundness theorems. We will also review quickly a new approach for building symbolic models described by G. Bana and H. Comon-Lundh in 2012. * Title borrowed from Abadi and Rogaway's paper in 2000.

Exposés passés (2012-2013)

Mardi 3 juillet 2012
Flavien Breuvart (PPS)
Tests mutuellement récursif et adéquation complète

On se propose ici de caractériser totalement la propriété d'adéquation complète pour le lambda calcul dans les K-models, une sous classe de la sémantique stable. Étant donné un objet réflexif, nous allons voir qu'il est possible d'enrichir la syntaxe du lambda-calcul avec les points de celui-ci. Les effets enrichissants la syntaxes permettent alors trivialement la définissabilité des points du modèle. Nous allons ensuite étudier les propriétés propres de ces extensions, qui peuvent notamment se réduire en une extension finie et très intéressante dans le cas ou le modèle est finement engendré. Enfin nous allons voire ce que l'étude de ce sur-calcul nous apprend sur le calcul original et comment, par une dérivation syntaxique (mais qui peut être interprétée en terme de jeux), on peut caractériser l’adéquation complète et sa négation.

Mardi 26 juin – Relâche

Mardi 19 juin 2012
Victoria Lebed (IMJ)
Homologies of Algebraic Structures via Braidings

The aim of this talk is to add an intermediate step " -> braiding -> " to the usual scheme algebraic structure -> differential complex from homology theory. The advantages of this viewpoint will be discussed. Appropriate braidings for vector spaces, associative and Leibniz (= "non-commutative Lie") algebras, and self-distributive structures will be constructed, recovering familiar homologies. Representations of these structures will also be treated in a braided way. All the constructions will be effectuated in an (eventually preadditive) monoidal category and illustrated diagrammatically. If the time permits, our homologies will be given a quantum shuffle interpretation. All necessary reminders will be made.

Jeudi 14 juin 2012 à 14h en salle 0D09
John Baez (UC Riverside)
Stochastic Petri Nets and Chemical Reactions

Chemists use "chemical reaction networks" to describe random interactions between things of different types. These are essentially the same as what computer scientists call "stochastic Petri nets". From such a structure, we can obtain a differential equation describing time evolution. A simple criterion implies that this equation has stationary solutions. This criterion involves a generalization of Euler characteristic to stochastic Petri nets.

Mardi 12 juin 2012 en salle 0D07
Après-midi thématique sur la théorie des types homotopiques

de 14h à 15h
Ieke Moerdijk (Radboud University, Nimègue, Pays-Bas)
Classifying spaces and Voevodsky's univalence axiom

Voevodsky has proposed a new axiom for type theory, the so-called univalence axiom. I will give a proof of the validity of this axiom for the interpretation of type theory in simplicial sets, based on some basic facts from the theory of classifying spaces.

de 15h à 15h30
Pause café

de 15h30 à 16h30

François Lamarche (LIX)
Une sémantique pour la théorie des types de Martin-Löf dans la catégorie des petites catégories

Nous présentons un modèle pour le type identité de Martin-Lôf qui donne aussi les produits dépendants. La sémantique que nous présentons a aussi l'avantage d'être concrète (en particulier il n'y a aucun besoin pour des système de factorisation, même si on peut en introduire si on veut) et d'être facile à calculer.

La catégorie de base est celle des petites catégories. Il y a déjà presque vingt-cinq ans j'ai remarqué que les bifibrations—les foncteurs qui sont à la fois des fibrations de Grothendieck et des opfibrations—possédaient les produits dépendants dans cette catégorie, et donc qu'on pouvait y modéliser l'essentiel de la théorie de Martin-Löf. Il restait à trouver un endofoncteur des chemins sur Cat qui était lui-même une bifibration et engendrait celles-ci par une action, du genre de celle qui donne lieu aux fibrations de Hurewicz dans les espaces topologiques. L'aspect géométrique de la construction de ce foncteur est frappant ; de plus il ressemble à la "construction du hamac" de Dwyer-Kan, sans coïncider avec celle-ci. En particulier il montre beaucoup de promesses pour simplifier les calculs d'homotopie dans Cat. Un autre aspect intéressant de ce foncteur est qu'il semble entrer dans le cadre axiomatique des "Path Objects" récemment proposé par Garner et van Der Berg.

Mardi 5 juin 2012
Willem Heijtljes (LIX)
Proof nets and semi-star-autonomous categories

Girard's original proof nets are a canonical graphical presentation of proof in multiplicative linear logic without units. In capturing their categorical semantics, the question is how to treat proof nets with a single conclusion, which would normally be captured by morphisms out of the monoidal unit I. However, proof nets that do include the monoidal unit are not canonical for the semantics of star-autonomous categories. We address this issue via a set-valued functor called the /virtual unit/, which takes the place of hom(I,-). Then proof nets are canonical for a notion of /semi-star-autonomous category/ incorporating this functor. This is joint work with Lutz Strassburger.

Mardi 29 mai 2012
Simona Ronchi della Rocca (Università di Torino)
A complete polynomial lambda-calculus

This work is in the field of Implicit Computational Complexity. One of the aims of Implicit Computational Complexity is the design of programming languages with bounded computational complexity. In fact, guaranteeing and certifying a limited resources usage is of central importance for various aspects of computer science. One of the more promising approaches to this aim is based on the use of lambda-calculus as paradigmatic programming language, and on the design of type assignment systems for lambda-terms, where types guarantee, besides the functional correctness, also the desired complexity bound. In this spirit, some systems characterizing polynomial time complexity have been designed, inspired by the Light Logics. The problem of these characterizations is that, while the systems are functionally complete, their expressivity is very small, in the sense that few algorithms can be coded. In particular, a proper subset of strongly normalizing terms can be typed. We propose a system of stratified typed, inspired by intersection types but without associativity, which is correct and complete for polynomial time computation, while typing all the strongly normalizing terms, so increasing the expressivity w.r.t. the previous proposals.

Mercredi 9 mai 2012 à 11h en salle 0D04
Michael Warren (Institute of Advanced Studies, Princeton)
Towards type theoretic models of homotopy types

In this talk we give a type theoretic definition of weak infinity groupoid and investigate the homotopy theoretic properties of such weak infinity groupoids. It is a non-trivial problem to show that such type theoretic weak infinity groupoids are a model of homotopy types and even in order to model homotopy n-types for small n requires the development of new techniques. We will describe these techniques and the resulting models of homotopy n-types for small n. We expect that suitable generalizations of these techniques can be used to give a model of all homotopy types and to provide a positive answer to Voevodsky's conjecture regarding the constructive character of the univalence axiom.

Jeudi 3 mai à 16h en Salle 5D91
Andrei Akhvlediani (University of Oxford)
A general framework for Categorical Universal Algebra

Categorical Universal Algebra uses many different gadgets to formalise the idea of a theory. Examples include plain operads, symmetric operads and Lawvere theories. In this talk, we explore a framework for formulating and analysing such gadgets in general. We shall show that all the above examples of theories become internal monads in Kleisli categories for (extensions of) familiar 2-monads on Cat.

In the second part of the talk, we focus on understanding how relationships between types of theories lead to relationships between theories of these types. To do this, we shall analyse the equivalence between pseudo. distributive laws and extensions. This analysis will allow us to define a functor from theories of one type to theories of another type.

Vendredi 30 mars 2012 (en salle 5C03)
10h30 – Ed Morehouse

Adjunction Based Categorical Logic Programming

From its beginnings with PROLOG, logic programming was rooted in classical logic and the semantics of model theory. The work of Dale Miller, Frank Pfenning, Roy Dyckhoff and others has been instrumental in bringing about the shift to a more proof-theoretical perspective, allowing the exploration of operational semantics for proof search in other logics, notably, intuitionistic and linear.

Largely independently, much progress has been made in providing categorical interpretations for various logical systems. One strand within this work began with Lawvere's observation that the connectives of first-order intuitionistic logic all have natural descriptions by adjoint functors.

We will pursue this idea to show how the inference rules of Gentzen's natural deduction and sequent calculus, as well as some of their properties, such as harmony, can be derived from the connectives' adjoint descriptions in a uniform way. We will then explore the effect of connective chirality on proof search and finish by sketching a categorical operational semantics of proof search suitable for logic programming.

Mardi 27 mars 2012 (séance double)

10h – Michele Abrusci (Roma Tre)
Pi^1_2 Logique

11h – Pause

11h15 – Wouter Stekelenburg (Utrecht University)
From Relative to Classical Realizability

Realizability structures assign subsets of a partial combinatory algebras to formulas. In relative realizability, we pick a set of special combinators; a formula is only valid, if the structure assigns a set of combinators that contains some of these special combinators. With minor adaptations, relative realizability interpretations are sound for a more general sort of combinatory algebra I call `lazy partial combinatory algebra'. Lambda terms ordered by weak head reducibility form an example of lazy partial combinatory algebras. We can `implement' Krivine's machine on a lazy partial combinatory algebra and use that implementation to build classical realizability structures. The construction is related to the negative translation.

Vendredi 23 mars 2012
10h30 – Thomas Streicher
Isomorphic Types are Equal!

In disciplines like algebra or topology one tends to consider isomorphic structures as sort of equal. As opposed to set theory this is possible in intensional Martin-Loef type theory whose identity types endow each type with the structure of a weakly infinite dimensional groupoid. Motivated by this observation we will show how to interpret types as Kan complexes and families of types as Kan fibrations. Finally, we will formulate Voevodsky's Univalence Axiom expressing that isomorphic types are equal.

Mardi 20 mars 2012
David Baelde (ITU Copenhagen)
Formal Proofs of Robustness for Watermarking Algorithms

I will present some new results on the security of watermarking schemes against arbitrary attackers, and their full formalization in Coq. This is joint work with P. Courtieu, D. Gross-Amblard and C. Paulin, as part of the ANR project Scalp which focuses on formal proofs of probabilistic algorithms.

Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data.

We present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking.

Mardi 13 mars 2012 en salle 1C18
Thomas Streicher (TU Darmstadt)
Krivine's Classical Realizabiliy from a Categorical Perspective

We show how Krivine's classical realizability gives rise to a tripos

and ensuing classical realizability topos. We discuss how assemblies look like in this framework. Moreover, we give a more general notion of realizability structure which also can be organized into a tripos and ensuing topos.

Mardi 24 janvier 2012
Paul-André Melliès (PPS)
Braided notions of dialogue categories

A dialogue category is a monoidal category equipped with an exponentiating object. In this talk, I will introduce a notion of braided dialogue category, and explain how this notion clarifies the topological nature of game semantics and of linear continuations.

Mardi 17 janvier 2012
Etienne Duchesne (LIPN)
MELL in a free compact closure

The categorical presentation of the standard model of the geometry of interaction –namely the free compact closure of sets and partial injections Int(PInj)– fails to be a denotational semantics of MELL. The work of Melliès, Tabareau & Tasson on the formula for a free exponential modality gives us insights into the reasons of this failure: absence of free pointed objects, absence of equalizers of some groups of permutations... We will present generic constructions which successively add the algebraic structure needed to compute this formula, and show that the usual model of GoI wrapped in these successive layers defines a denotational semantics of MELL.

Mardi 20 décembre 2011
Camell Kachour (Université de Sydney)
Approche algébrique des oméga-groupoïdes faibles

Dans cet expose nous décrivons une monade sur la catégorie des oméga-graphes dont les algèbres sont des oméga-groupoides faibles. L'un des concepts clé qui nous permet d'obtenir cette monade est la notion d'oméga-graphes involutifs qui est aux oméga-graphes ce que les graphes involutifs (au sens de Berger-Mellies-Webber) sont aux graphes. On montre qu'en dimension 1 les algèbres pour cette monades sont des groupoides, et qu'en dimension 2, les algèbres pour cette monade sont des bigroupoides. En particulier

on montre qu'en dimension 2, les 1-cellules sont des équivalences.

In this talk we describe a monad on the category of the omega-graphs which algebras are weak omega-groupoids. A key concept which allows to obtain this monad is the notion of involutive omega-graphs which is for the omega-graphs what involutive graphs (in the sense of Berger-Mellies-Webber) are for graphs.

We show that in dimension 1, algebras for this monad are groupoids, and in dimension 2, algebras for this monad are bigroupoids. In particular we show that in dimension 2, the 1-cells are equivalences.

Mardi 13 décembre 2011
Benedikt Ahrens (Université de Nice)
Initiality for Typed Syntax and Semantics

We give an algebraic characterization of syntax with a semantics in form of reductions. A language is specified in two steps: a signature specifies the terms and types of the language, and inequations over the signature specify reduction rules on those terms. To any signature S with a set of inequations A we associate a category of "models" and show that this category has an initial object deserving to be called "syntax associated to S with reductions according to A". Some of the initiality theorems are implemented in Coq, yielding a machinery which allows to easily obtain syntax, certified substitution and reductions according to specifications provided by the user.

Mardi 6 décembre 2011
Lutz Strassburger (LIX)
Normalization for Classical Logic by Breaking Paths in Atomic Flows

In this talk, I present a novel cut elimination procedure for classical propositional logic. It is based on the recently introduced atomic flows: they are purely graphical devices that abstract away from much of the typical bureaucracy of proofs. We make crucial use of the "path breaker", an atomic-flow construction that avoids some nasty termination problems, and that can be used in any proof system with sufficient symmetry. I will show some relations to two-dimensional rewriting.

Mardi 29 novembre 2011
Danko Ilik (Université de Stip)
Continuation-passing-style models, once more

Continuations were invented in the semantics of programming languages as means to reason about

effectfull computation by reasoning about the rest of the current computation. They are also useful as a proof technique, allowing one to prove normalization(-by-evaluation) for proper extensions of simply typed lambda-calculus. Previously, it has been show how they can be used to show NBE for lambda-calculus with strong sums, giving rise to a notion of model which resembles Kripke models, the basic structure being the same, but where the notion of forcing of non-atomic formulas is changed. They can also be used to show NBE for delimited control operators whose answer type is a single global sigma-0-1 formula. Logically, this is interesting because it permits to give a normalisation proof for intuitionistic logic extended with the Double-negation Shift schema, and to show that it remains constructive.

After revising this previous work, I will show how to extend this method to the hierarchy of delimited control operators from Danvy-Filinski's "Abstracting Control", thereby obtaining an NBE proof for those operators on an arbitrary number of sigma-0-1 formulas. In the process, it is suggested how to change the reset-rule, making it more polymorphic, so that the NBE proof goes through. I will also outline how one can give a proof that NBE normalizes according to the expected reduction rules for a calculus, but just in the case of lambda-calculus with sums.

Mardi 22 novembre 2011
Nicolas Tabareau (INRIA)
Forcer le calcul des constructions

Dans cet exposé, je présenterai des travaux en cours sur une traduction de forcing pour CoC inspirée des travaux de Krivine et Miquel [LICS'11] mais aussi des travaux sur des modèles de préfaisceaux de Birkedal et al. [LICS'11]. Cette traduction de forcing permettrait par exemple de définir des inductifs généraux dans Coq mais aussi de définir des logiques augmentées avec une notion de monde (à la Kripke) pour décrire des relations logiques pour des langages avec références d'ordre supérieur et des (first-class) continuations.

Mardi 15 novembre 2011
Samuel Mimram (CEA)
A Non-Standard Semantics for Kahn Networks in Continuous Time

In a seminal article, Kahn has introduced the notion of process network and given a semantics for those using Scott domains whose elements are (possibly infinite) sequences of values. This model has since then become a standard tool for studying distributed asynchronous computations. From the beginning, process networks have been drawn as particular graphs, but this syntax is never formalized. We take the opportunity to clarify it by giving a precise definition of these graphs, that we call nets. The resulting category is shown to be a fixpoint category, i.e. a cartesian category which is traced wrt the monoidal structure given by the product, and interestingly this structure characterizes the category: we show that it is the free fixpoint category containing a given set of morphisms, thus providing a complete axiomatics that models of process networks should satisfy. We then use these tools to build a model of networks in which data vary over a continuous time, in order to elaborate on the idea that process networks should also be able to encompass computational models such as hybrid systems or electric circuits. We relate this model to Kahn's semantics by introducing a third model of networks based on non-standard analysis, whose elements form an internal complete partial order for which many properties of standard domains can be reformulated. The use of hyperreals in this model allows it to formally consider the notion of infinitesimal, and thus to make a bridge between discrete and continuous time: time is "discrete", but the duration between two instants is infinitesimal. Finally, we give some examples of uses of the model by describing some networks implementing common constructions in analysis. This is joint work with Romain Beauxis.

Mardi 8 novembre 2011
Nicolas Guénot (LIX)
The Focused Calculus of Structures

In order to harness the great expressivity offered by the calculus of structures, and use it as a reasonable setting for proof search, we have transplanted the focusing technology from the sequent calculus into the system LS for full linear logic in the calculus structures. After a brief introduction to the calculus of structures, I'll show how the use of a polarised syntax (introducing shifts at phase changes) leads to a focused system, and explain how such a system relates to the usual focused sequent calculus. Then, I'll present our focusing proof (that is, completeness of the focused restriction with respect to the unrestricted system), which is surprisingly simple, using inductions to refine any given proof into a focused proof. (joint work with Kaustuv Chaudhuri and Lutz Strassburger)

Mardi 11 octobre 2011
Jerome Simeon (IBM T.J. Watson Research Center, Scalable XML Integration Infrastructure)
Monadic Formulation of Database Algebras (Database Optimization for Web 2.0 Queries)

Support for data processing is becoming a "must have" for programming languages targeting Web 2.0 and Cloud development. The data support in those languages (Microsoft's Linq, University of Edinburgh's Links, EPFL's Scala, Yahoo!'s Pig Latin, IBM's JAQL, etc) is usually based on monads or comprehensions. Those capture the expressive power of SQLiterators, brings a well understood semantics, type system, andfunctional rewrites. At the compiler level, however, they are at odds with database optimizers which mostly rely on relational (or nested-relational) algebras. That mismatch was embarrassingly on display throughout the design of XQuery, the XML query language, whose semantics

is based on monads, and for which most implementations target relational backends. We propose a alternative semantic formulation of XQuery, which is also based on monads, but has a precise correspondence with compilation into a database algebra. The claim is that this alternative formulation provides key insights into the nature of database compilers that can provide a stepping stone for the integration of database and programming languages. We leverage that insight in two ways. First we show that type systems for database algebras require an original solution to the old problem of subtyping with record concatenation. Second we use it to provide a formal semantics and optimizations for XQuery extended with side-effects.

Mardi 4 octobre 2011
Eduardo Bonelli (UNQ and CONICET)
Justification Logic and History Based Computation

Justification Logic (JL) is a refinement of modal logic that has recently been proposed for explaining well-known paradoxes arising in the formalization of Epistemic Logic. Assertions of knowledge and belief are accompanied by justifications: the formula $\valid{t}{A}$ states that $t$ is ``reason'' for knowing/believing $A$. We study the computational interpretation of JL via the

Curry-de Bruijn-Howard isomorphism in which the modality $\valid{t}{A}$ is interpreted as: $t$ is a type derivation justifying the validity of $A$. The resulting lambda calculus is such that its terms are aware of the reduction sequence that gave rise to them. This serves as a basis for understanding systems, many of which belong to the security domain, in which computation is history-aware

Mardi 13 septembre 2011 à 11h
Jan Hoffmann (LMU, Munich)
Polynomial Amortized Resource Analysis

Concrete (non-asymptotic) resource bounds have many important applications in software development but their manual determination is tedious and error-prone. As a result, the automatic computation of concrete resource bounds is desirable and has been extensively studied.

For my PhD I have developed the first type-based resource analysis that automatically infers polynomial resource bounds for functional programs. As pioneered by Hofmann and Jost for linear bounds, I rely on the potential method of amortized analysis.

The analysis is generic in the resource of interest and can derive

bounds on time and space usage. It is fully automatic if a maximal

degree of the bounding polynomials is given. The bounds are naturally closed under composition and eventually summarized in closed, easily understood formulas.

In my talk, I explain the basic ideas of this automatic amortized analysis using simple examples from functional programming. I then demonstrate the capabilities and limitations of the system by analyzing more involved programs with our prototype implementation. Finally, I present an experimental evaluation that shows that the computed bounds are often asymptotically tight and that the constant factors are close or even identical to the optimal ones.

You can find further info and try out the analysis on the project's web page: http://raml.tcs.ifi.lmu.de

Mardi 20 septembre 2011 à 11h
Nikos Tzevelekos (University of Oxford)
Games with names

The dynamic creation of new resources is a ubiquitous feature in modern computing and emerges in a wide range of scenarios: from process calculi and the semantics of mobility, to programming languages with objects, references, exceptions, etc. These resources are identified by use of unique, fresh identifiers which we call names. This talk is about formal techniques for reasoning about names which have emerged in the last years.

We will focus on game semantics, a denotational theory of programming languages which models programs as interactions (games) between two players, representing the program and its environment respectively. Nominal games constitute a fresh strand of the theory which is founded on a universe of sets with names called nominal sets. Such games provide models for programming languages with new resources such as fragments of ML. Moreover, nominal game models can be given algorithmic representations by means of newly introduced abstract machines, called Fresh-Register Automata, which operate on infinite alphabets of names.

Archives (2010-2011)

Mardi 5 juillet à 14h en salle 5A092 (sous-marin)
Dominique Duval (Université Joseph Fourier, Grenoble)
Etats et exceptions considérés comme des effets duaux

Dans cet exposé je présenterai un résultat inattendu : il existe une symétrie entre les effets calculatoires liés aux états et aux exceptions. Cette symétrie prolonge la dualité bien connue entre les produits et les coproduits. Plus précisément, les opérations "lookup" et "update" pour les états sont duales, respectivement, des opérations "throw" et "catch" pour les exceptions. Cette approche fournit un nouveau point de vue sur les états et les exceptions, qui permet de contourner les problèmes dus à la non-algébricité du traitement des exceptions. (En collaboration avec J.-G. Dumas, L. Fousse et J.-C. Reynaud.)

States and exceptions considered as dual effects

In this talk I will present a surprising result: there exists a symmetry between the computational effects of states and exceptions, based on the well-known categorical duality between products and coproducts. More precisely, the lookup and update operations for states are respectively dual to the throw and catch operations for exceptions. This approach gives rise to a new point of view on states and exceptions, which bypasses the problems due to the non-algebraicity of handling exceptions. (Joint work with J.-G. Dumas, L. Fousse and J.-C. Reynaud.)

Mardi 7 juin à 11h
Pino Rosolini (Università di Genova)
Quotients in Hyperdoctrines

We apply tools from categorical logic to give an abstract description of constructions used to give models of theories for constructive mathematics based on intensional type theory. We show that the key concept is that of an elementary hyperdoctrine in the sense of Lawvere and we describe a notion of quotient completion as a left biadjoint to a fairly natural forgetful 2-functor. Instances of that notion are the exact completion on a category with products and weak pullbacks as well as models of various extensional type theories.

Journée thématique sur la combinatoire diagrammatique et la catégorification

Lundi 30 mai à Chevaleret, en salle 1C12.

de 10h30 à 12h30 en salle 1C12
Aaron Lauda (Columbia University)
Diagrammatic categorification of quantum groups (première partie)

Quantum groups play an important role in knot theory, representation theory, and statistical mechanics. In particular, the Jones polynomial is a famous knot invariant that can be understood in terms of the representation theory of the quantum group associated to the Lie algebra sl2 of traceless 2x2 matrices. This description facilitated a vast generalization of the Jones polynomial to other quantum link and tangle invariants called Reshetikhin-Turaev invariants. These invariants, which arise from representations of quantum groups associated to simple Lie algebras, subsequently led to the definition of quantum 3-manifold invariants. In these talks we categorify quantum groups using a simple diagrammatic calculus that requires no previous knowledge of quantum groups. These diagrammatically categorified quantum groups not only lead to a representation theoretic explanation of Khovanov homology but also inspired Webster's recent work categorifying all Reshetikhin-Turaev invariants of tangles.

de 12h30 à 14h
Pause déjeuner

de 14h à 15h30 en salle 1C12
Heather M. Russell (Louisiana State University)

Springer Varieties and Knot Theory

Springer varieties are studied because their cohomology carries an action of the symmetric group, and their top-dimensional cohomology is irreducible. Khovanov's work on categorified tangle invariants brought to light surprising connections between crossingless matchings, two row Young tableaux, and a certain class of these varieties.
We expand these combinatorial and topological relationships to a larger class called two-row Springer varieties and give a completely diagrammatic construction of the Springer representation which can be expressed skein theoretically. If time permits, we will discuss our current work extending these results to three-row Springer varieties as well as connections to sl_3 link invariants.

de 15h30 à 16h
Pause café et discussion libre

de 16h à 17h30 en salle 1C12
Aaron Lauda (Columbia University)
Diagrammatic categorification of quantum groups (deuxième partie)

Mardi 31 mai à 11h en salle 5C03
Olivia Caramello (University of Cambridge)
The unification of Mathematics via Topos Theory

I will propose a new view of Grothendieck toposes as unifying spaces in Mathematics being able to serve as 'bridges' for transferring information

between distinct mathematical theories. This approach, first introduced in my Ph.D. dissertation, has already generated ramifications into different mathematical fields and points towards a realization of Topos Theory as a unifying theory of Mathematics. In the talk, I will explain the fundamental principles that characterize my view of toposes as unifying spaces, and demonstrate the technical usefulness of these methodologies by providing applications in several distinct areas including Model Theory, Proof Theory, Algebra, Geometry and Topology.

Marcredi 1er juin à 11h en salle 1C12
Olivia Caramello (University of Cambridge)
A topos-theoretic approach to Stone-type dualities

I will present an abstract topos-theoretic machinery for building Stone-type dualities; several well-known dualities are recovered as applications of the

machinery to specific sets of inputs, and many new dualities are introduced. I will also discuss how our topos-theoretic interpretation can be exploited to obtain results connecting properties of preorders and properties of the

corresponding locales or topological spaces, and indicate how adjunctions between various kinds of categories can be established as natural applications of our general methodology. This work represents a concrete implementation of the abstract methodologies of unification of Mathematics via Topos Theory presented in a previous talk.

Mardi 24 mai à 11h
Paul-André Melliès (PPS)
Une introduction à la logique tensorielle

La logique tensorielle est une logique primitive qui raffine la logique linéaire, et l'unifie à la sémantique des jeux et au calcul des continuations. Dans cet exposé qui se veut introductif, nous expliciterons les principes fondamentaux de cette logique, ainsi que les liens qu'elle entretient avec la logique linéaire et les variantes polarisées (LC, LLP, ludique,

calcul des piles) qui ont vu le jour ces vingt dernières années. Si le temps le permet, nous décrirons une présentation algébrique de la logique tensorielle,

ainsi qu'une notion de réseau de démonstration de nature purement topologique, au croisement de la logique linéaire, de la sémantique des jeux, et de la théorie des noeuds.

Mardi 26 avril à 11h
Thomas Ehrhard (PPS)
Un calcul classique de piles

On présentera un calcul classique à base de piles dérivant du lambda-mu calcul de Parigot, un système de typage pour ce calcul, ses propriétés opérationnelles (Church-Rosser, normalisation) et sa sémantique dénotationnelle.

Travail commun avec Alberto Carraro et Antonino Salibra (Univ. Ca' Foscari de Venise).

Mardi 19 avril à 11h
Etienne Duchesne (LIF)
The geometry of multiplicatives and additives: interaction and orthogonality

We present a denotational semantics of multiplicative linear logic based on the geometry of interaction. In that semantics, we can define polymorphism using a construction similar to the one of history-free game semantics. We can also present the standard longtrip criterion of

proof-nets as an orthogonality relation in the sense of Hyland and Schalk [HS03], and build a category of orthogonality which provides a fully complete model of MLL (without mix). Besides we extend these constructions – polymorphism and orthogonality –, to the interpretation of additive connectives.

Jeudi 31 mars à 11h en salle 0C02
Stéphane Zimmermann (PPS)
Connecteurs Synthétiques en Logique Linéaire Différentielle

Afin d'obtenir une ludique pour la logique linéaire différentielle, un bon début est d'avoir des connecteurs synthétiques. On commencera par montrer un résultat de focalisation pour la logique linéaire différentielle, en s'attachant à souligner ce que la partie différentielle change au problème, puis à partir de ce système focalisé on montrera comment écraser les groupes de règles obtenus sans perte d'information afin d'obtenir un calcul de connecteurs synthétiques.

Mardi 29 mars 2011 à 11h
Marcelo Aguiar (Texas A&M University)
Hopf monoids. An introduction with examples

The notion of Hopf monoid models the manner in which combinatorial structures compose and decompose. This talk will introduce the notion and illustrate it through a number of examples of combinatorial and geometric flavor. These include the Hopf monoid of faces of the Coxeter complex and the Hopf monoid of generalized permutahedra. We will focus on the antipode problem and its implications (time permitting).

Jeudi 24 mars 2011 à 10h en salle 5A92 (sous-marin)
Pierre Clairambault (University of Bath)
Isomorphisms of types in the presence of higher-order references

Abstract: We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterising isomorphisms of types in a finitary language L_2 with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of L_2 with natural numbers.

Mardi 15 mars 2011 à 11h
Maurice Herlihy (Brown University)
The Index Lemma and the Zero-One Exclusion Task

We consider a family of simple distributed coordination tasks, parameterized by an $n$-bit vector $v$, where $n+1$ is the number of proceses. Processes are asynchronous. At the beginning, some subset of the processs wakes up. Those processes communicate with one another using a shared read-write memory, and

eventually halt with a binary value. If $0< k< n+1$ processes participate, they cannot all output $b[k]$. If all processes participate, they cannot all output the same value.

We use the Index Lemma to derive a characteristic value for each instance of the family, with the property that the problem cannot be solved if the characteristic is non-zero. Curiously, the characteristic is non-zero "most of the time", but there are sporadic values for which it is zero. It remains an open question whether these instances of zero-one exclusion are solvable.

Joint work with Eli Gafni

Mardi 22 mars 2011 à 11h
Ryu Hasegawa (Tokyo University)
System LC and a semantic proof of the Church-Rosser property

Traditionally, categories are used to provide the denotational semantics of type systems. This procedure ignores the dynamic aspect of computation. Reductions on the side of type systems are translated into equalities on the side of categories.

In this work, we incorporate the notion of reductions into a category. We introduce System LC. It is a computational system directly built on the linear category, a categorical counterpart of the linear logic.

We show the Church-Rosser property of System LC. The idea for a proof is use of a combinatorial enumeration model. It is adaption of the Joyal-Girard's analytic functor model to the linear logic. Using its enumerative property, we give a semantic proof.

Mardi 22 février 2011 de 11h à 12h30
Tom Hirschowitz (LAMA, Université de Chambéry)
Une ludique pour CCS?
(travail en collaboration avec Damien Pous, CNRS)

Au début, on voulait faire un début de ludique pour CCS, dans le sens une sémantique de jeux, pour laquelle on définit une notion d'équivalence observationnelle par orthogonalité. Mais CCS est un langage concurrent, donc la notion habituelle de stratégie est trop grossière. Du coup, l'approche proposée est à mi-chemin entre la ludique et les travaux de Joyal, Nielsen et Winskel sur les préfaisceaux comme modèles de la concurrence. On va même plus loin que les préfaisceaux, puisque la notion d'innocence est interprétée comme une condition de faisceau, pour une topologie adéquate. On montre ensuite que nos stratégies forment un champ, dans lequel le recollement de deux stratégies s'interprète comme leur interaction. Grâce à ça, on définit une notion générale de critère d'observation (sans doute pas dans sa forme finale), chaque critère induisant par orthogonalité une notion d'équivalence. On considère enfin deux instances concrètes, correspondant respectivement au "fair" et au "must" testing, dont on montre qu'elles coïncident (alors qu'elles diffèrent dans le cadre habituel).

Journées thématiques sur les modèles du calcul des constructions
5ème étage, 23 avenue d'Italie, Paris 13ème.

Lundi 14 février 2011, salle rose
11h: Alexandre Miquel, Classical realisability for the Calculus of Constructions
13h30: Andreas Abel, Normalisation-by-Evaluation for the Calculus of Constructions
15h: Bruno Barras, Formalizing a set-theoretical model of CIC in Coq/IZF (part I)

Mardi 15 février, salle rose
10h: Marc Lasson, Realizability and Parametricity in Pure Type systems
11h: Hugo Herbelin, What needs to be changed in CIC to make it compliant with Voevodsky's univalent model
11h30: Jeff Sarnat, Logical relations for sequent calculus with guarded (co)recursion
14h: Bruno Barras, Formalizing a set-theoretical model of CIC in Coq/IZF (part II)

Mardi 8 février 2011 à 11h
Gianluigi Bellin (Université de Vérone)
De Parigot à Crolard et encore à Parigot: Déduction naturelle et term assignment pour la logique co-intuitioniste

Das son paper Free Deduction: An Analysis of "Computations" in Classical Logic LNCS 592, 1990, M.Parigot présenta un système qui extendait soit la Deduction Naturelle soit le Calcul des Sequents, très approprié pour la Deduction naturelle à plusieur conclusions. Mais dans ses travaux suivants Parigot donna le lambda-mu calcul domme interprétation computationnelle del la Free Deduction, c'est à dire, un système extendant le lambda calcul avec des operateurs de control, parfaitement correspondant à la Deuction Naturelle de Prawitz pour la logique classique (1965).

Dan ses travaux sur la logique bi-intitioniste (logique intuitioniste ou classique avec la soustration) T.Crolard utilise le Lambda-mu calcul. Mais si on veut étudier la logique co-intuitionniste, la syntaxe la plus naturelle, et parfaitement duale de la logiquen intuitioniste, est une deduction naturelle "sequent style" avec une seule formule dans l'antécedent et plusieurs formules dans le succédent et une interpretation computationnelle "distribuée". On peut voir ça comme un retour à l'esprit de la Free Deduction. Mais c'est le calcul des sequents avec formule de queue qui est en correspondence bijective avec les arbres de preuve de Prawitz pour la deductio naturelle NJ de l'implication et de la conjonction.

Une peculiarité de ce calcul, qui est une contributiona aux fondaments logiques de la computation distribuée, est l'absence d'instruments pour determiner le scope des binders, ce qui est fait dans le pi-calcul par le nu-operateur. Ici les variables liées sont remplacées par des fonctions et on peut parler de "remote binding" and "remote substitutions".

Des motivations linguistiques et philosophiques pour l'etude de la logique co-intuitioniste sont les proprietées logiques des operateurs de "conjecture" et d'"hypothese".

Mardi 18 janvier 2011 à 11h
Alexandre Pilkiewicz
The essence of monotonic state

We extend a static type-and-capability system with new mechanisms for expressing the promise that a certain abstract value evolves monotonically with time; for enforcing this promise; and for taking advantage of this promise to establish non-trivial properties of programs. These mechanisms are independent of the treatment of mutable state, but combine with it to offer a flexible account of “monotonic state”.

Mardi 11 janvier 2011 à 11h

Beniamino Accatolli
The kingdom of polarity and the polarity of the kingdom

The aim of the talk is to present a study on a local and implicit notion of box for Linear Logic Proof-Nets, i.e., a notion of box which is not given, but induced by correctness and enjoying a local algorithm for its reconstruction. We start by showing that in Multiplicative Linear Logic there is no hope of obtaining such a notion, and so Linear Logic Proof-Nets cannot admit local implicit

boxes. We then show that in a certain polarized setting, it is possible to decorate the net with some additional edges, called jumps, so that the smallest subnet having as conclusion a given positive formula P, called the kingdom of P, admits a local and implicit definition. We conclude by showing a mismatch between polarity inducing implicit boxes and polarity as in Polarized Linear Logic.

Mardi 14 décembre 2010 à 11h
Timothy G. Griffin (University of Cambridge)
Routing in Equilibrium

Some path problems cannot be modelled using semirings because the associated algebraic structure is not distributive. Rather than attempting to compute globally optimal paths with such structures, it may be sufficient in some cases to find locally optimal paths—- paths that represent a stable local equilibrium. For example, this is the type of routing system that has evolved to connect Internet Service Providers (ISPs) where link weights implement bilateral commercial relationships between them. Previous work has shown that routing equilibria can be computed for some non-distributive algebras using algorithms in the Bellman-Ford family. However, no polynomial time bound was known for such algorithms. In this talk, we show that routing equilibria can be computed using Dijkstra’s algorithm for one class of non-distributive structures. This provides the first

polynomial time algorithm for computing locally optimal solutions to path problems.

This is joint work with João Luís Sobrinho

presented at the 19th International Symposium on Mathematical Theory of Networks and Systems (MTNS 2010). You can find the paper here.

Mardi 7 décembre 2010 à 11h
Tobias Heindel
The Good Behaviour of the Typical Colimits in Extensive, Regular, and Adhesive Categories

A common phenomenon in extensive, regular, and adhesive categories can be described roughly as follows: certain colimits "survive in the universe of spans". Moreover this phenomenon captures "the essence" of these categories; e.g., a category with pullbacks is extensive if and only if coproducts exist and are preserved by the graphing functor into the span category.

Assuming only familiarity with basic category theory, the talk focusses on the paradigmatic case of Van Kampen pushouts in adhesive categories. The main ideas of the characterisation of their good behaviour are presented using partial map categories instead of span bicategories (even though this corresponds to a weaker property). A noteworthy open problem is the characterisation of all "well-behaved" pushouts/colimits in toposes, which are the main example of adhesive categories.

Mardi 7 décembre 2010 à 14h en salle 5A92 (sous-marin du 5ème étage)
Benno van den Berg
An introduction to Algebraic Set Theory

Algebraic set theory was introduced by Joyal and Moerdijk in their book from 1995 and is an approach to the semantics of set theory based on categorical logic. One of its strengths is that it gives a uniform approach to set theories of different kinds (classical and constructive, predicative and impredicative). In addition, it allows one to capture different kinds of semantics (forcing, sheaves, boolean-valued models, realizability) in one common framework. In this talk, I will give an introduction to the subject, concentrating on main ideas rather than technical details.

Mardi 23 novembre 2010 à 11h
Marc Lasson
Réalisabilité et paramétricité dans les PTS

Je décrirai une méthode systématique pour construire une logique à partir d'un lambda-calcul typé décrit comme un système de types pur (PTS). Cette logique, elle-même présentée sous forme de PTS, fournit des formules pour exprimer des propriétés des termes. Elle offre ainsi un cadre adéquat pour développer une théorie de la paramétricité

ainsi qu'une théorie de la réalisabilité du langage d'origine. Enfin, grâce à la généralité des PTS, je montrerai comment paramétricité et réalisabilité s'avèrent être inter-définissables dans ce cadre.

Mardi 23 novembre 2010 à 14h en 5A92 (sous-marin du 5ème étage)
Alex Simpson (Université d'Edimbourg)
Towards an observational view of computational effects

In the theory of "algebraic" computational effects, proposed by Plotkin and Power, effects are modelled algebraically via "operations" and "equations" (that is, in the terminology of universal algebra, via "generators" and "relations"). The "operations" are the computational primitives that trigger effects. The "equations" implement behavioural equality between programs built out of operations alone.

It is traditional in computer science to obtain behavioural equality as a derived notion, defined as the contextual equivalence induced from a set of primitive "observations" on computations. In this talk, I will discuss the beginnings of an approach to implementing effects by taking "operations" and "observations" as the primitive notions, rather than "operations" and "equations".

This is work in progress. The completed part appeared in LICS 2010, in a paper coauthored with Patricia Johann and Janis Voigtlaender.

Lundi 25 octobre 2010 à 14h en salle rose (23, avenue d'Italie, 5ème étage)
Ulrich Berger
Program extraction from proofs using induction and coinduction

In this talk I discuss two examples of program extraction from proofs using induction and coinduction.

The first example belongs to the realm of computable analysis: a coinductive predicate characterising "approximable" real numbers is defined, and from proofs of closure properties of C_0 one extracts implementations of arithmetic operations with respect to the signed digit representation of real numbers. This example has been done in Coq in collaboration with Sylvain Dailler.

In the second example I show how to extract monadic parser combinators from proofs that certain labelled transition systems are finitely branching. While in the first example coinduction is central, here

induction features prominently because finiteness is an inductive concept.

Both examples have in common that the proofs used for program extraction can be carried out in rather simple formal systems, namely mild extensions of first-order logic. One reason for this is that the data types the extracted programs operate on (infinite digit streams, higher-order functions) need not be formalized, but are extracted automatically from the proven formula. This indicates that the perspective of replacing programming by the activity of proving is not as daunting as it seems, and that therefore program extraction

might become an attractive method for producing formally certified programs in the future.

Mardi 19 octobre 2010 à 11h
Thomas Colcombet, Clemens Ley et Gabriele Puppis
Théorème de Schützenberger et ensembles nominaux, sur le mode informel

Tout ce que vous avez toujours voulu savoir sur la théorie des automates et le théorème de Schützenberger, sans jamais oser le demander... tout cela dans le cadre faisceautique des ensembles nominaux.

Mardi 12 octobre 2010 à 11h
Rasmus Møgelberg
Full abstraction of the linear state monad translation

The enriched effect calculus (EEC) is a type theory suitable for reasoning about linear usage of effects. In this talk I show how to use it as a target language for the linear state monad translation, translating terms in a call-by-value source language to terms in EEC treating a state type linearly. If time permits I will show that this translation is fully abstract. The syntactic result is based on a semantic analysis, and along the way we will discuss a general notion of models of EEC and the relationship to monads and models of Dual Intuitionistic/Linear Logic.

This is joint work with Jeff Egger, Alex Simpson and Sam Staton

Mardi 5 octobre 2010 à 11h
Paul-André Melliès
Une introduction aux théories algébriques

Dans cet exposé qui se veut introductif, j'expliquerai comment (1) décrire de manière purement algébrique (et aussi diagrammatique) la structure sous-jacentes aux monades d'états, (2) comment généraliser la notion de théorie algébrique pour décrire des systèmes comme le lambda-calcul. Ma présentation s'appuiera sur le travail de Gordon Plotkin et John Power ainsi que sur mon article récent à LICS sur la condition de Segal et les effets calculatoires.

Mardi 28 septembre 2010 à 10h
Marco Gaboardi (Universite de Bologne)
Definability and Full abstraction for a Linear PCF

I present some recent results obtained in joint works with Luca Paolini and Mauro Piccolo. I first introduce SlPCF*, a linear core of PCF extended by basic primitives related to exception handling and nondeterministic evaluation, and I show that it is fully abstract for a linear model in the category of coherence spaces and linear functions. Then I show that the full abstraction result can be used to prove that the standard contextual equivalence can be handled by considering simpler observational equivalences. Finally, I show that the semantic linearity provides crucial information for the evaluation of programs by presenting a concrete evaluation machine for SlPCF that prunes efficiently the evaluation space.

Mardi 28 septembre 2010 à 11h
Kai Brunnler (Bern University)
An Algorithmic Interpretation of a Deep Inference System

Our original goal was to find a term calculus that corresponds to a deep inference system in the same way as the lambda calculus corresponds to a natural deduction system. What we found happens to be system of categorical combinators, similar to Curien's, but based on a different presentation of a CCC which is in a certain sense more symmetric and more fine-grained. This also leads to different reduction properties, in particular our system is locally confluent. Normalisation and confluence are open problems. A more conceptual question is how the extra "fine-grainedness" could be useful computationally. (Joint work with Richard McKinley.)

Archives (2009-2010)

Mardi 22 juin 2010 à 11h
Alexis Bernadet (LIX)
Strongly normalising terms and non-idempotent intersections types

We introduce a notion of typing with non-idempotent intersection types and a few applications. The typing systems we present all provide a characterisation of strong normalizing terms, and interact well with orthogonality techniques. We first treat the pure lambda calculus and then a calculus with explicit substitutions. This calculus provides a better control on resources, which allows us to derive finer results on complexity: we can finely tune the typing so as to measure the exact lengths of maximal reductions.

Mardi 6 juillet 2010 à 11h
Robin Cockett (Calgary University)
Faa di Bruno categories

For Cartesian differential categories the chain rule is a consequence of the composition in the "bundle category" which is a simple fibration. This talk generalizes this situation using the higher-order chain rules originally developed by Faa Di Bruno in the nineteenth century, to produce a fibration Faa(\X) -> \X which is, in fact, the counit of a comonad on the category of left additive categories. Cartesian differential categories then arise precisely as coalgebras of this comonad.

Mardi 15 juin 2010
Jacob Vosmaer (ILLC, UvA)
Powerlocales via relation lifting
(joint work with Yde Venema and Steve Vickers)

The Vietoris powerlocale is the point-free version of the Vietoris hyperspace construction for topological spaces. Vietoris hyperspaces have a strong implicit connection with modal logic. We show how using modern

techniques from coalgebraic modal logic (using the so-called cover modality) and relation lifting (i.e. the process of lifting endofunctors on the category of sets and functions to endofunctors on the category of sets and relations), one can define a generalized T-powerlocale construction, given T, an endofunctor* on the category of sets. We show that the T-powerlocale construction preserves regularity and regularity+compactness*, and that if we choose T to be the finite power set functor, we obtain the classical Vietoris construction.

(* under reasonable technical restrictions)

Mardi 8 juin 2010 à 11h
Sylvain Salvati (LABRI)
Extending Recognizability to the Simply Typed lambda-Calculus

The simply typed lambda-calculus can be seen as generalization of both strings and trees. As sets of such lambda-terms appear in various contexts, it seems rather natural to bridge the ideas of formal language theory to the study of those sets. As a first step in that direction, we introduce a notion of recognizable sets of simply typed lambda-terms as a generalization of the usual notions of recognizable sets of strings and trees. The main interest of this extension is that it is closed under beta-eta equality which brings computation in the realm of language theory. We will generalize the usual constructions for automata so as to obtain the usual closure properties of recognizable sets under boolean operations and inverse homomorphisms. The closure under inverse homomorphism of recognizable sets of lambda-terms has many interesting applications that are underpinned by the closure of recognizable sets under beta-eta equality. In particular it gives several results about the class of context free languages of lambda-terms and also gives a rather simple proof of decidability of 4th order matching.

Mardi 1er juin 2010 à 11h
Michele Abrusci (Roma 3)
Quelques thèmes de la théorie de la démonstration du XXe siècle (Partie II)

Après-midi thématique sur la géométrie différentielle synthétique

de 14h à 15h30 en salle 1C06
Anders Kock (Aarhus University, Danemark)
Combinatorial differential forms

This talk will be concerned with a simple coordinate free synthetic version of the algebra of differential forms. It will include a section concerned with algebraic theories (in the sense of Lawvere) which have the "Fermat property"; this property gives a rigorous basis of some aspects of differential calculus, prior to the Newton-Leibniz era.

de 15h30 à 16h
Pause café

de 16h à 17h30 en salle 1C06
Jacques Penon (Université Paris Diderot)
De l'infinitésimal au local

Dans cet exposé, Jacques Penon nous donnera une présentation panoramique du travail qu'il a mené au cours de sa Thèse d'Etat.

Mardi 25 mai 2010 à 11h
Marie Bjerrum (Cambridge University)

General distributivity

It is a well established fact that filtered colimits commute with finite limits in the category of sets and a few articles treat other mixed interchange properties (distributivitive laws) in Set such as finite products commuting with so-called sifted colimits, and finite connected limits commuting with pseudofiltered colimits etc. Abstractly we can determine necessary and sufficient conditions for a small colimit to commute with a given small limit in the category of sets (work by C.Lair and F.Foltz in "Diagrammes"). But it is not immediate to subtract from this any classification of the concrete distributive laws. However by looking at special cases we get a more complete picture of this Galois correspondence between the classes of limits and colimits that commute, even if we don't yet have complete transparency. (This is PhD-work in progress).

Après-midi thématique sur la géométrie différentielle synthétique

de 14h à 15h30 en salle 1C06

Anders Kock (Aarhus University, Danemark)
Synthetic geometry of manifolds

If the number line has sufficiently many nilpotent elements, any manifold acquires an interesting structure, first considered in algebraic geometry, namely the neighbourhoods of the diagonal. Using a synthetic language, this provides a useful way of talking about the differential geometry in combinatorial terms.

Litterature. Anders Kock, Synthetic Geometry of Manifolds, Cambridge University Press 2010.

de 15h30 à 16h
Pause café et discussion libre

Mardi 27 avril 2010 à 11h

Julianna Zsido (Université de Nice)
Syntaxe abstraite non typée

Je présenterai l'approche de Fiore, Plotkin & Turi à la syntaxe abstraite avec liaison de variables. Elle est formulée dans le language des catégories et des préfaisceaux (contravariants). Ensuite je présenterai l'approche de Hirschowitz & Maggesi qui est une variante de la première mais basée sur les notions de monade et de module. Finalement je présenterai une traduction entre ces deux approches.

Jeudi 15 avril 2010 à 14h (en salle 0D01)
Jason Reed (University of Pennsylvania)
Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy

We want assurances that sensitive information will not be disclosed when aggregate data derived from a database is published. Differential privacy offers a strong statistical guarantee that the effect of the presence of any individual in a database will be negligible, even when an adversary has auxiliary knowledge. Much of the prior work in this area consists of proving algorithms to be differentially private one at a time; we propose to streamline this process with a functional language whose type system automatically guarantees differential privacy, allowing the programmer to write complex privacy-safe query programs in a flexible and compositional way.

The key novelty is the way our type system captures function sensitivity, a measure of how much a function can magnify the distance between similar inputs: well-typed programs not only can't go wrong, they can't go too far on nearby inputs. Moreover, by introducing a monad for random computations, we can show that the established definition of differential privacy falls out naturally as a special case of this soundness principle. We develop examples including known differentially private algorithms, privacy-aware variants of standard functional programming idioms, and compositionality principles for differential privacy.

Mardi 30 mars 2010 à 11h
Shinya Katsumata (RIMS, Université de Kyoto)
A categorical geometry of interaction for additives

We propose a categorical GoI-style interpretation of multiplicative additive linear logic (MALL). The main feature of our approach is to employ a categorical structure called semibiproducts for interpreting additive connectives. We show that an instance of our categorical interpretation with Pfn coincides with what Mairson and Rival's token machine computes on MALL proofs. We also present a method to gather slicewise interpretation of MALL proofs to obtain the interpretation that is invariant under cut elimination.

(Joint work with Naohiko Hoshino.)

Mardi 30 mars 2010 à 14h (en salle 0C02)
David Baelde (Université du Minnesota)
Finite automata and regular fixed point formulas in muMALL

We present muMALL, an extension of multiplicative additive linear logic with least and greatest fixed points, and illustrate its expressiveness through the model-checking problem of non-deterministic finite automata inclusion.

We consider encoding automata as least fixed points in muMALL, and use its general induction scheme to reason about them. We provide a coinductive characterization of inclusion that yields a natural bridge to proof-theory. This yields a completeness theorem, but can also be generalized to the fragment of "regular formulas", obtaining new insights about inductive theorem proving and cyclic proofs in particular.

Jeudi 1er avril 2010 à 14h (en sous-marin, salle 6A92)
Alessandra Palmigiano (ILLC, Universiteit van Amsterdam)
Topological groupoid quantales: a non-etale setting

Quantales are ordered algebras which can be thought of as

pointfree noncommutative topologies. In recent years, their connections have been studied with fundamental notions in noncommutative geometry such as groupoids and C*-algebras. In particular, the setting of quantales corresponding to etale groupoids has been very well understood: a bijective correspondence has been defined between localic etale groupoidsand inverse quantale frames. We present an equivalent but independent way of defining this correspondence for topological etale groupoids and we extend this correspondence to a non-etale setting.

Mardi 23 mars 2010 à 11h
Mircea Dan Hernest (IMAG, Grenoble)
Modal Functional Interpretation

We extend Goedel’s Dialectica interpretation to modal formulas and prove it sound for a certain modal arithmetic based on Goedel’s T. The range of this Modal Dialectica

interpretation is the usual Heyting Arithmetic in all finite types. We illustrate the use of the new tool for optimized program extraction as part of an enhanced light Dialectica interpretation in the sense of Hernest and Trifonov.

Vendredi 19 mars 2010 à 16h (en salle 7D01)
Thomas Streicher (TU Darmstadt)
Homotopy Models of Type Theory and Voevodsky's Equivalence Axiom

In structural mathematics (category theory and alike) one tends to consider isomorphic structures as equal. In a paper from the 1990s Martin Hofmann and I suggested an axiom which added to type theory expresses this desire. This is made possible by the weakness of Martin-Loef's puzzling identity types.

Recently Voevodsky has suggested a stronger so called Equivalence Axiom which is motivated by a homotopy model within the topos of simplicial sets which I considered in 2006. What is new is an interpretation of universes as suggested by Voevodsky.

In my talk I'll try to both explain the Equivalence Axiom and sketch the homotopy model.

Vendredi 12 mars 2010 à 17h (en salle 6C01)
Thomas Streicher (TU Darmstadt)
A Synthetic Theory of Sequential Domains

Cartwright, Curien and Felleisen in the 1990s identified the wellpointed category OSA of observably sequential algorithms. Since OSA admits a universal object realizability over the typed pca OSA gives rise to a topos RT(OSA). In OSA there is the game O with one question and no answer. Axiomatizing the structure of O within RT(OSA) gives rise to a synthetic theory of sequential

domains. This allows one to reason within RT(OSA) about OSA as sets with certain properties.

(travail en collaboration avec Bernhard Reus)

Mardi 9 mars 2010 à 11h
Arnaud Spiwack (LIX)

Higher Categories: Beyond Internal Categories

I will indulge in a rather speculative talk, where I will expose stuff I know I don't know. I will present higher categorical problems, araising from Bishop style mathematics, which have applications in computer checked mathematics and, possibly (hopefully?), in programming language design. In both case the focus is dependent type theory. These problems cannot be solved by defining higher categories by means of internal algebras (as in T. Leinster, for instance), essentially because we need categories which are not sets (and additive categories which are not groups, though it is not a focus of this talk). I will then engage in the description of some ideas to approach these problems, which may also serve as pretext for various digressions and fruitful discussions.

Mardi 2 mars 2010 à 11h
Simona Ronchi della Rocca (Université de Turin)
Call-by-value vs call-by-name

A new characterization of strong normalization in lambda calculus, both in the lazy and non lazy setting, will be presented, through two call-by-value lambda calculi. Standard (cbn) lambda calculus of Church and call-by-value (cbv) lambda calculus of Plotkin are paradigmatic calculi modeling respectively the

cal-by-name and call-by-value parameter passing. While they share the same syntax, their semantics is quite different, in particular the notion of normal form is meaningless in the cbv. A key notion in this setting is that of value and the more general one of potential valuability: a term is potentially valuable if and only if it reduces to a value under a suitable substitution. This notion allows for characterizing the solvable terms in cbv and for establish an interesting bridge between the two languages: the set of potential valuable terms in cbv coincides with the set of strongly normalizing terms in cbn, equipped with the lazy operational semantics. Starting from this connection, we define a further call-by-value lambda calculus, where the notion of value is different from that of Plotkin, such that the set of potentially valuable terms in it coincides with the strongly normalizing terms in cbn lambda calculus, equipped with the usual operational semantics. The common technical tool used for these characterizations is based on intersection types.

Mardi 23 février 2010 à 11h
Brigitte Pientka (McGill University)
Beluga: programming with dependent types, contextual data, and contexts

The logical framework LF provides an elegant foundation for specifying formal systems and proofs and it is used successfully in a wide range of applications such as certifying code and mechanizing meta-theory of programming languages. However, incorporating LF technology into functional programming to allow programmers to specify and reason about formal guarantees of their programs from within the programming language itself has been a major challenge.

In this talk, I present an overview of Beluga, a framework for

programming and reasoning with formal systems. It supports specifying formal systems in LF and it also provides a dependently typed functional language that supports analyzing and manipulating LF data via pattern matching. A distinct feature of Beluga is its direct

support for reasoning with contexts and contextual objects. Taken together these features lead to powerful language which supports writing compact and elegant proofs.

Mardi 2 février 2010 à 11h
Vincent Padovani (PPS)
Le probleme du "Ticket Entailment"

La question de la decidabilite du "Ticket Entailment" est le second probleme de la liste des problemes ouverts de TLCA (http://tlca.di.unito.it/opltlca). Il s'agit de determiner s'il existe un algorithme de decision pour le fragment de la logique propositionnelle obtenu a partir des quatre schemas d'axiomes suivants et du modus ponens :

(I) a -> a (B) (a -> b) -> ((c -> a) -> (c -> b))

(B') (a -> b) -> ((b -> c) -> (a -> c))

(W) (a -> (a -> b)) -> (a -> b)

Malgre sa formulation tres simple, ce probleme - issu de travaux en logique modale remontant aux annees 60 - est ouvert depuis 1973. On peut lui trouver plusieurs formulations equivalentes - probleme d'habitation en logique combinatoire ou dans un fragment du lambda-calcul simplement type, probleme de l'existence d'un theoreme de compacite pour une semantique ad-hoc, etc. Je tenterai de vous montrer en quoi cette question est, en depit des apparences, inhumainement difficile, et presenterai quelques resultat partiels.

Mardi 19 janvier 2010
Attention: séance double

de 10h à 11h en salle 0C02
Clement Houtman (LORIA, Universite Henri Poincaré)

Towards a focused treatment of theories

In most proof systems, theories such as Peano arithmetic, real numbers or set theory are usually represented by unstructured multisets of axioms written in an ad hoc logical language. Some exceptions propose to transcend the axiom/inference division. Such systems include Huang's assertion level, Schroeder-Heister's definitional reflection, Negri and Von Plato's non-logical rules or superdeduction modulo. The latter stands on the duality between computation and reasoning known as Poincaré's Principle. It allows systematic translation of deductive axioms into custom inference schemes. The user automatically obtains a higher-level specific deduction system that leads to enhanced proof-search procedures for example. This process of turning an

axiomatic theory into some custom deduction system is sound but not always complete. Cut-elimination may also be lost. Therefore it is essential to express criteria ensuring the good behaviour of the obtained systems. First I will explain how such completeness and cut-admissibility results for superdeduction depend on certain synchrony hypotheses. Then I will express polarization procedures that modify the presentation of a theory so that these synchrony hypotheses hold. Combined with the superdeduction paradigm, the polarization procedures ensure either completeness or cut-admissibility. Finally I propose to reforge superdeduction on top of the focusing paradigm so that polarization is no longer required.

de 11h15 à 12h30 en salle 6C01
Thomas Ehrhard (PPS)
Espaces de finitude et topologies linéaires: quelques petites choses qu'on n'a pas le temps de dire d'habitude: deuxième partie.

Mardi 12 janvier 2010 à partir de 14h30
Après-midi thématique sur la théorie des opérades

de 14h30 à 16h en salle 0C05
Benoît Fresse (Laboratoire Paul Painlevé, Lille)
Modules sur les opérades, modèles de foncteurs entre catégories d'algèbres sur les opérades.

• Bref rappel : opérades et algèbres sur une opérade. PB : construction de modèles effectifs pour des foncteurs entre catégories d'algèbres associées à des opérades.
• Foncteurs de puissances symétriques à coefficients et réponse au PB posé.
• Exemples fondamentaux : algèbres enveloppantes, formes différentielles.
• Opérations.
• Théorèmes d'invariance homotopique.
• Un exemple d'application : ce qui marche pour des algèbres commutatives continue de marcher pour des algèbres E-infini (commutatives à homotopie près).

de 16h à 16h30 en salle 0D04
Pause café

de 16h30 à 18h
Adrian Tanasa (Centre de Physique Théorique, Ecole Polytechnique)
Algebres de Hopf combinatoires dans les theories quantiques des champs noncommutatives

Nous introduirons l'espace noncommutatif de Moyal et une maniere avec laquelle on peut y construire des theories quantique des champs. Une maniere pertinente pour representer ces theories est en utilisant des graphes a rubans. La renormalisabilite de ces modeles est rendue difficile par l'apparition d'un nouveau type de divergence non-locale. Malgre cela, nous verrons plusieurs manieres de definir des modeles renormalisables. Cette nouvelle renormalisabilite noncommutative peut etre decrite par une structure d'algebre de Hopf a la Connes-Kreimer adapte pour ces graphes a rubans.

Mardi 5 janvier 2010 à 11h
Stéphane Lengrand (LIX, Ecole Polytechnique)
Provability modulo Theory

(travail en collaboration avec Germain Faure, Chantal Keller et Assia Mahboubi)

Je commencerai par presenter les objectifs du projet PSI (Proof-Search in Interaction with domain-specific methods). Je rappelerai alors l'architecture SMT (SAT-modulo-theory) qui organise, avec un certain succes, l'interaction entre du raisonnement purement logique, d'une part, et du raisonnement specifique a une certaine theorie, d'autre part. Nous verrons ensuite dans quelles directions nous envisageons de generaliser le principe de fonctionnement de SMT ou de l'adapter a la theorie de la demonstration et aux assistants de preuves. La problematique principale est la gestion des quantificateurs. Nous verrons au passage certaines connexions avec la deduction modulo.

Mardi 15 décembre 2009 à 11h
Paul-André Melliès (PPS)
Algèbre laxe sur une monade 2-dimensionnelle

Dans cette exposé de nature introductive, j'expliquerai comment généraliser la notion de monade à une notion d'algèbre laxe sur une 2-monade. J'expliquerai aussi comment cette notion permet de repenser et de généraliser la construction traditionnelle du produit parallèle (par) en logique linéaire à une situation où la négation n'est plus involutive.

Mardi 8 décembre 2009 à 11h
Marc Bagnol et Anne-Sophie de Suzzoni (ENS)
Vers un modèle quantique de la logique linéaire

Les espaces cohérents quantiques de J.-Y. Girard sont une tentative de relecture du modèle "historique" de la logique linéaire, les espaces cohérents, dans le langage de l'information quantique. La construction avait cependant été abandonnée, car elle ne pouvait pas fonctionner sur des espaces de Hilbert de dimension infinie.

Au cours de notre mémoire de M2, nous avons étés amenés à proposer des modifications au modèle initial, qui le rendent plus proches de la mécanique quantique et plus facilement extensible à la dimension infinie.

On présentera les bases de la construction et les points où elle diffère avec les espaces cohérents quantiques usuels. Puis on verra quelques questions que pose ce modèle "quantique" de la logique linéaire en cours de construction.

Mardi 8 décembre 2009 à 14h, en salle 0D09
Benoît Valiron (Grenoble)
Higher-Order in Quantum Computation.

A theorem in quantum computation states that for any (first-order) algorithm, measurements can always be performedat the end of the computation. An interpretation of this fact is that a quantum algorithm can be mainly be regarded as a unitary map.

This has forced two approaches to higher-order quantum computation. The first approach is mixing higher-order structures, measurements and unitaries in a same algorithm. This leads to a semantics based on completely positive maps. The other approach follows the spirit of the theorem and considers higher-order structures as base states of some Hilbert space and tries to capture the computation as a unitary operation.

In this talk I shall compare these two approaches.

Vendredi 4 décembre 2009 à 15h30, en salle 7D01
Thomas Streicher (TU Darmstadt)
Realizability vs. Forcing

In his work on classical realizability for second order logic and set theory J.-L. Krivine has emphasized that he considers realizability as a generalization of Cohen forcing. From a topos-theoretic perspective this is

puzzling since the overlap of realizability and sheaf toposes consists (up to equivalence) just of Set.

To clarify the situation we give a more axiomatic presentation of Krivine's classical realizability and show how it subsumes forcing (using ideas from

Girard's phase semantics).

Finally we compare it with the notion of ordered pca as introduced by P.Hofstra and J.van Oosten and discuss how this latter notion allows one to iterate realizability constructions which is needed in yet unpublished work by Krivine on realizing the set-theoretic axiom of choice.

Mardi 1er décembre 2009 à 11h
Gabriel Kerneis (PPS)
Compiler des threads à l'aide de continuations en C

L'utilisation de continuations pour représenter et compiler des threads est une technique classique dans le monde des langages fonctionnels. Elle est en revanche quasiment inexistante pour les langages impératifs.

CPC (Continuation Passing C [1]) est un compilateur source-source qui transforme, à l'aide d'une conversion CPS, des programmes écrits dans un dialecte de C augmenté de primitives de concurrence en programmes C équivalents. Nous montrerons toutes les difficultés générées par un langage impératif en appel par valeur, qui ne dispose ni de fonctions de première classe ni à plus forte raison de continuations, et comment les contourner tout en produisant des programmes efficaces.

Cet exposé sera l'occasion de présenter deux petits résultats originaux sur le lambda-lifting et la conversion CPS, qui garantissent la correction des transformations effectuées par CPC.

[1] http://www.pps.jussieu.fr/~jch/software/cpc

Jeudi 26 novembre 2009 à 14h en salle 5A92
Carlos Lombardi (Université Quilmes et Université Buenos Aires)
Proof terms for infinitary term rewriting

(travail en collaboration avec Eduardo Bonelli, Alejandro Rios et Roel de Vrijer)

Proof terms were proposed as a formal framework allowing to reason about equivalence of reductions in term rewriting systems (TRSs). In this talk we will first survey proof terms for finitary TRSs. We will then discuss a possible extension to infinitary rewriting, including a pertinent notion of permutation equivalence.

Mardi 24 novembre 2009 à 11h
Jade Alglave (Equipe Moscova, INRIA Rocquencourt)
Fences and Synchronisation Idioms in Weak Memory Models.

Understanding the behaviour of a program running on a multiprocessor requires a precise definition of the underlying memory system and the behaviour of the processors involved: the memory model. We present a generic axiomatic framework, implemented in the Coq proof assistant, to define weak memory models in terms of several parameters: local reorderings of reads and writes, and visibility of inter and intra processor communications through memory, including full store atomicity relaxation.

Thereby, we give a formal hierarchy of weak memory models, in which we provide a formal study of what should be the action and placement of fences to restore a given model – such as Sequential Consistency (SC) – from a weaker one.

We provide furthermore formal requirements for abstract locks that guarantee SC

semantics to data race free programs. Moreover, we provide an abstract definition of atomic primitives on which crucial pieces of code such as lock implementations build, and study their interaction with the barriers appearing in their code. This allows us to show that a particular implementation of locks matches these requirements.

Mardi 24 novembre 2009 à partir de 14h en salle 5C12
Après-midi thématique sur la théorie des opérades

de 14h à 15h30
Benoît Fresse (Laboratoire Paul Painlevé, Lille)
Modules sur les opérades, modèles de foncteurs entre catégories d'algèbres sur les opérades.

• Bref rappel : opérades et algèbres sur une opérade. PB : construction de modèles effectifs pour des foncteurs entre catégories d'algèbres associées à des opérades.
• Foncteurs de puissances symétriques à coefficients et réponse au PB posé.
• Exemples fondamentaux : algèbres enveloppantes, formes différentielles.
• Opérations.
• Théorèmes d'invariance homotopique.
• Un exemple d'application : ce qui marche pour des algèbres commutatives continue de marcher pour des algèbres E-infini (commutatives à homotopie près).
  

de 15h30 à 16h
Pause café

de 16h à 17h30
Muriel Livernet (Laboratoire Analyse, Géométrie et Applications, Paris 13)
Algèbres pré-Lie.

Après des définitions et exemples je présenterai des résultats classiques concernant les algèbres pré-Lie, leur lien avec les arbres enracinés et l'algèbre de Hopf de Connes et Kreimer ainsi que la formule de Butcher. Puis je présenterai des résultats plus récents sur les algèbres pré-Lie libre et l'algèbre de Lie des arbres enracinés.

Mardi 17 novembre 2009 à 10h30 en salle 4C17
François Pottier (Equipe Gallium, INRIA Rocquencourt)
De ML à F_omega avec sortes récursives: une traduction monadique bien typée.

La traduction monadique bien connue explicite le tas et le fait circuler à travers les calculs sous forme d'un argument et résultat supplémentaires. Si le langage de départ est doté de références et de fonctions de première classe, comme c'est le cas en ML, alors il est particulièrement difficile de comprendre de quel système de types on doit doter le langage cible pour pouvoir argumenter que cette traduction produit des programmes bien typés. Je présenterai une solution à ce problème, en choisissant pour langage cible une version de F_omega dotée de certaines sortes récursives.

Mardi 10 novembre 2009 à 11h

Thomas Ehrhard (PPS)
Espaces de finitude et topologies linéaires: quelques petites choses qu'on n'a pas le temps de dire d'habitude.

Mardi 20 octobre 2009 à 11h
Ralph Matthes (IRIT)
Un plongement du fragment appel par nom du calcul lambda-mu-mu-tilde dans le lambda-calcul simplement typé.

Mardi 13 octobre 2009 à 11h
Thibaut Balabonski (PPS)
Optimality in the Weak Pure Pattern Calculus.

Pattern matching is usually seen as an extension of the core theory of functional programming. It is thus out of the scope of most theoretical works on efficient evaluation or optimality, since those are restricted to lambda-calculus. This talk is about efficiency and sharing of computation in the Pure Pattern Calculus, a framework which integrates pattern matching as a base mechanism. We will see how an analysis of the calculus can lead to the description of an interesting implementation. Indeed, we will have a formal account of its efficiency by proving it optimal with respect to some given restrictions on the reduction space.

Mardi 5 octobre 2009 à 11h
Paul-André Melliès (PPS)
Introduction à la théorie des opérades (suite).

Pour cette séance, je propose de poursuivre mon introduction à la théorie des opérades, en expliquant (1) les rapports que cette théorie entretient avec la notion de déformation par homotopie, et (2) la construction d'une monade des états locaux par générateurs et relations.

Mardi 29 septembre 2009 à 11h
Marc de Falco (PPS)
De la programmation des réseaux d'interaction à leur statut algébrique.

Dans un premier temps on partira d'un problème très concret, présenté dans notre article [1], qui est celui de la représentation explicite des réseaux d'interaction. Explicite ayant un sens proche de celui que l'on retrouve dans les substitutions explicites, c'est-à-dire une représentation directement implémentable. Notre solution, basée sur une variante très simplifiée de la Géométrie de l'Interaction, est très proche de travaux antérieurs de Kelly et Laplaza [2] sur la représentation canonique de la catégorie compacte close libre engendrée par une catégorie. Ainsi, dans un second temps, nous montrerons en quel sens les réseaux d'interaction sont une sorte de catégorie compacte fermée libre engendrée par une 2-catégorie libre. Au delà de l'extension de la présentation de Kelly et Laplaza, cela nous permettra de donner un sens algébrique à de nombreux aspects mystérieux des réseaux d'interaction : boucles, notion de sémantique par une généralisation des théories algébriques, ...
[1] : Marc de Falco, An Explicit Framework For Interaction Nets, RTA'09
[2] : G.M. Kelly and M.L. Laplaza, Coherence for compact closed categories, Journal of Pure and Applied Algebra 19, 1980

Mardi 22 septembre 2009 à 11h
Paul-André Melliès (PPS)
Introduction à la théorie des opérades.

• Contactez Paul-André Melliès ou Michele Pagani pour toute information concernant le groupe de travail.
  
• Abonnez-vous à notre liste de diffusion pour recevoir les annonces du groupe de travail.
  
• Consultez les archives décennales du groupe de travail (1999-2008).
  
• Suivez ces http://www.math.univ-paris-diderot.fr/ufr/batsophiegermain pour accéder au bâtiment Sophie Germain.