Preuves, Programmes et Systèmes

Groupe de travail Sémantique

Le groupe de travail se réunit à Chevaleret le mardi de 11h à 12h15 en salle 5C03.

Exposés à venir

Mardi 22 mai
François Lamarche (LIX)
TBA

Mardi 29 mai
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.

Mardi 29 mai
Willem Heijltjes (LIX)
TBA

Mardi 12 juin
Ieke Moerdijk (Radboud University)
TBA

Exposés passés (2011-2012)

Mercredi 9 mai à 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 (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 (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
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
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 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
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
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
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
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
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
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
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
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
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
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
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 à 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 à 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 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 conseils utiles pour accéder au site de Chevaleret.