11 décembre 2014, 14:00 : Séminaire

Guillaume Brunerie (Nice), Théorie des types cubique

Je présenterai des travaux en cours (en collaboration avec Dan Licata) sur le développement d’une théorie des types cubique, le but étant d’obtenir une théorie des types ayant de bonnes propriétés calculatoires (normalisation forte, canonicité, décidabilité du typage) tout en étant compatible avec la théorie des types homotopiques, en particulier avec l’axiome d’univalence et les types inductifs supérieurs. Ces travaux sont égalements très liés aux travaux de Thierry Coquand, Simon Huber et Marc Bézem sur un modèle constructif de la théorie des types homotopiques dans les ensembles cubiques.

5 décembre 2014, 10:30 : Soutenance de thèse

Michele Alberti (I2M/Focus), On operational properties of quantitative extensions of lambda-calculus

Jury:

  • Paul B. LEVY (University of Birmingham), Rapporteur
  • Simone MARTINI (Università di Bologna), Directeur
  • Michele PAGANI (Université Paris Diderot), Rapporteur
  • Laurent REGNIER (Aix-Marseille Université), Directeur
  • Simona RONCHI DELLA ROCCA (Università di Torino), Présidente

  • Emmanuel BEFFARA (Aix-Marseille Université), Directeur (invité)

  • Ugo DAL LAGO (Università di Bologna), Directeur (invité)
  • Lionel VAUX (Aix-Marseille Université), Directeur (invité)

Cette thèse porte sur les propriétés opérationnelles de deux extensions quantitatives du λ-calcul pur: le λ-calcul algébrique et le λ-calcul probabiliste. Dans la première partie, nous étudions la théorie de la β-réduction dans le λ-calcul algébrique. Ce calcul permet la formation de combinaisons linéaires finies de λ-termes. Bien que le système obtenu jouisse de la propriété de Church-Rosser, la relation de réduction devient triviale en présence de coefficients négatifs, ce qui la rend impropre à définir une notion de forme normale. Nous proposons une solution qui permet la définition d’une relation d’équivalence sur les termes, partielle mais cohérente. Nous introduisons une variante de la β-réduction, restreinte aux termes canoniques, dont nous montrons qu’elle caractérise en partie la notion de forme normale précédemment établie, démontrant au passage un théorème de factorisation.

Dans la seconde partie, nous étudions la bisimulation et l’équivalence contextuelle dans un λ-calcul muni d’un choix probabliste. Nous donnons une technique pour établir que la bisimilarité applicative probabiliste est une congruence. Bien que notre méthode soit adaptée de celle de Howe, certains points techniques sont assez différents, et s’appuient sur des propriétés non triviales de « désintrication » sur les ensembles de nombres réels. Nous démontrons finalement que, bien que la bisimilarité soit en général strictement plus fine que l’équivalence contextuelle, elles coïncident sur les λ-termes purs. L’égalité correspondante est celle induite par les arbres de Lévy-Longo, généralement considérés comme l’équivalence extensionnelle la plus fine pour les λ-termes en évaluation paresseuse.

4 décembre 2014 : Chocola à Marseille

Séminaire Chocola à Marseille, avec les soutenances de Marc Bagnol (le 4 décembre) et Michele Alberti (le 5 décembre).

11:00: Paul Blain Levy (Birmingham), Transition systems over games
14:00: Guillaume Geoffroy (ÉNS), (à préciser)
15:30: Kazushige Terui (RIMS, Tokyo), Some topics on hypersequents

4 décembre 2014, 9:30 : Soutenance de thèse

Marc Bagnol (I2M), On the Resolution Semiring

Jury:

  • Pierre-Louis Curien
  • Jean-Yves Girard (directeur de thèse)
  • Ugo dal Lago (rapporteur)
  • Paul-André Melliès
  • Myriam Quatrini
  • Ulrich Schöpp
  • Philip Scott (rapporteur)
  • Kazushige Terui

We study in this thesis a semiring structure with a product based on the resolution rule of logic programming. This mathematical object was introduced initially in the setting of the geometry of interaction program in order to model the cut-elimination procedure of linear logic. It provides us with an algebraic and abstract setting, while being presented in a syntactic and concrete way, in which a theoretical study of computation can be carried on.

We will review first the interactive interpretation of proof theory within this semiring via the categorical axiomatization of the geometry of interaction approach. This interpretation establishes a way to translate functional programs into a very simple form of logic programs.

Secondly, complexity theory problematics will be considered: while the nilpotency problem in the semiring we study is undecidable in general, it will appear that certain restrictions allow for characterizations of (deterministic and non-deterministic) logarithmic space and (deterministic) polynomial time computation.

2 décembre 2014

Journée Logique à Marseille organisée par Nicolas Olivetti et Luigi Santocanale.

27 novembre 2014, 11:00 : Séminaire

Thomas Seiller (IHÉS), Des invariants de cohomologie pour la complexité?

J'exposerai des résultats récents à l'intersection entre mes travaux sur les graphes d'interaction et ceux concernant la complexité.

Mon travail sur les graphes d'interaction m'a mené à une construction systématique de modèles de la logique linéaire basée sur la notion de « graphage » — des réalisations de graphes par des fonctions mesurables. Intuitivement, un graphage est un graphe dont les sommets sont des ensembles mesurables et les arêtes sont « réalisées » par des fonctions mesurables. Ces modèles sont caractérisés par un monoide de fonctions (mesurables) qui décrit les différents manières de réaliser une arête.

Je montrerai que le choix de ce monoide correspond à imposer des contraintes de complexité. Cette correspondance est illustrée par l'obtention de modèles de MALL avec des exponentielles (très) faibles où le type des prédicats sur les entiers binaires !Nat_2 ⊸ Bool caractérise des classes de complexité telles que les languages réguliers, L (logspace), NL, Ptime.

Ces résultats permettent d'envisager l'utilisation d'invariants de cohomologie pour étudier les classes de complexité.

20 novembre 2014, 11:00 : Séminaire

Étienne Duchesne (University of Bath), Un formalisme pour réduire la taille des preuves

La deep inference est un formalisme des preuves généralisant le calcul des séquents. Il permet d'exprimer plus de logiques d'une façon plus compacte. Je passerai en revue ses principales propriétés aux travers de la logique BV, la logique classique et les atomic flows. J'aborderai également les récentes tentatives de définir la substitution d'un atome par une dérivation en deep inference.

13 novembre 2014

Séminaire Chocola à Lyon.

23 octobre 2014, 11:00 : Séminaire

Marco Solieri (Paris 13 (LIPN) / Bologna (Focus)), Geometry of Resource Interaction – A Minimalist Approach

The Resource λ-calculus (RC) is a variation of the λ-calculus where arguments can be superposed and must be linearly used, and where reduction introduces formal sums on terms. Hence it is a model for non-deterministic and linear programming languages. But RC is also the target language of Taylor-Ehrhard expansion of λ-terms, a linearisation of the usage of arguments. In a strictly typed restriction of RC, we study the notion of paths on proof-nets and the property of persistency. We define a Geometry of Interaction (GoI) that is invariant under reduction, consequently characterises path persistency, and also accurately counts the number of addends being superposed in normal forms. This work intend to be the first step toward an higher destination: understanding and explicitly describing the relation between expansion and GoI.

16 octobre 2014

Séminaire Chocola à Lyon.

25 septembre 2014

Séminaire Chocola à Lyon.

23 juin 2014, 10:30 : Séminaire

François Métayer (PPS, Paris 7), Les orientaux de Street revisités par Burroni

La construction d’un nerf des ω-catégories, c’est-à-dire un foncteur de la catégorie des ω-catégories vers celle des ensembles simpliciaux repose sur l'existence d’une famille adéquate de simplexes orientés, définis par Street. J’expliquerai comment l’approche de Burroni simplifie la construction de ces objets à la combinatoire délicate, en exploitant les propriétés d’un foncteur des cylindres sur ω-Cat.

12 juin 2014, 14:00 : Séminaire

Clément Aubert (I2M), Programmation logique, unification et espace logarithmique

Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance preuve-programme fournit alors une façon innovante de représenter les entiers binaires comme des fonctions dialoguant avec les programmes. Les machines abstraites que l’on peut y encoder (les observations) peuvent naturellement être vues comme des machines à pointeurs, qui parcourent l’entrée sans la modifier. On montre alors que ces observations sont suffisamment expressives pour caractériser l’espace logarithmique, et que décider de l’acceptation d’un mot par une observation est réductible au problème d’acyclicité d’un graphe, un problème également en espace logarithmique.

Travail en collaboration avec Marc Bagnol, Paolo Pistone et Thomas Seiller

25 avril 2014, 11:00 : Séminaire

Laurent Poinsot (Paris 13), Sur le groupoïde de géométrie d'une variété équationnelle équilibrée

Patrick Dehornoy a construit un monoïde de fonctions partiellement définies sur une algèbre de termes sur un domaine d'opérateurs (signature) S, dit monoïde de géométrie, qu'il associe à toute variété équationnelle V de S-algèbres déterminée par une congruence équilibrée, i.e., pour laquelle deux termes équivalents possèdent les mêmes ensembles de variables. Dans cet exposé je dégagerai la nature profonde de cette construction qui est celle d'un groupoïde. Je montrerai que celui-ci n'est que l'image d'un groupoïde plus fondamental par une représentation fidèle (un foncteur fidèle dans le groupoïde des ensembles et bijections). Ce dernier gouverne alors la "géométrie" du calcul dans la variété V, au sens où son action sur un terme correspond à des réécritures (au sens de la réécriture de termes), et hérite de surcroît d'une structure fonctorielle de S-algèbre. Si le temps me le permet, j'aborderai la généralisation de cette construction obtenue en remplaçant l'algèbre des termes par une algèbre libre dans une variété équationnelle déterminée par une congruence "linéaire".

18 avril 2014, 11:00 : Séminaire

Marc Lasson (Cambridge), Canonicity of groupoids laws using parametricity theory

The synthetic approach to weak ω-groupoids promoted by the univalent foundation program is the idea that (homotopy) type theory should be the primitive language in which spaces, points, paths, homotopies are derived. Following this approach, spaces are represented by types, points by inhabitants and paths by equalities between points (also known as identity types) and algebraic properties of these objects should not be unforced a priori (for instance by axioms) but should be derived directly from the language. Following this approach requires to be convinced that definitions of new operations should be canonical, in the sense that no important choice should be made by picking an implementation of these operations instead of an other. Identities, inversion and concatenation of path, associativities, idempotency of inversion, horizontal and vertical compositions of 2-paths, are all examples of groupoid laws.

Parametricity has been introduced by Reynolds to study the polymorphic abstraction of system F. It refers to the concept that well-typed programs cannot inspect the type their arguments; they must behave uniformly with respect to abstract types. Reynolds formalizes this notion by showing that polymorphic programs satisfy the so-called logical relations defined by induction on the structure of types. Dependent type systems are expressive enough to state their own parametricity theory.

In this talk, we will focus on the consequences of this remark when applied to identity types and we will use it to prove that all implementations of a given groupoid law are provably equal to each other.

9 avril 2014, 14:00 : Séminaire

Date et heure à confirmer en fonction de l'école au CIRM.

Alejandro Díaz-Caro (INRIA Rocquencourt & Paris Ouest), Type theory modulo isomorphisms

We defined a typed lambda-calculus where the isomorphisms between types are raised to the level of an equality relation. To this end, an equivalence relation is settled at the term level. We provide a proof of strong normalisation modulo such an equivalence, which is a non-trivial adaptation of the reducibility method. This work opens several paths for future work, which I will try to detail in this talk.

28 mars 2014, 14:00 : Séminaire

Benoît Valiron (PPS, Paris 7), Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi

In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model model of linear logic. We first define a simple, finite PCF-like lambda-calculus with booleans, and then we discuss two finite models, one based on finite sets and the other on finite vector spaces. The first model is shown to be fully complete with respect to the operational semantics of the language. The second model is not complete, but we develop an algebraic extension of the finite lambda calculus that recovers completeness. The relationship between the two semantics is described, and several examples based on Church numerals are presented.

18 mars 2014, 11:00 : Séminaire

Benedikt Ahrens (IRIT, Toulouse), Category theory in the Univalent Foundations

The Univalent Foundations is an extension of Intensional Martin-Löf Type Theory (MLTT) recently proposed by V. Voevodsky. Its novelty is the Univalence Axiom which implements the idea that indistinguishable types should be equal by identifying equality of types with isomorphism of types. When formalizing category theory in traditional, set-theoretic foundations, a significant discrepancy between the foundational notion of "sameness" - equality - and its categorical notion arises: most category-theoretic concepts are invariant under weaker notions of sameness than equality, namely isomorphism in a category or equivalence of categories. We show that this discrepancy can be avoided when formalizing category theory in Univalent Foundations. In this talk I first give an introduction to Voevodsky's Univalent Foundations. Afterwards I define categories and univalent categories within Univalent Foundations, and develop basic category theory. The two main results of our work are the following:

  1. Two univalent categories are equivalent (in the category-theoretic sense) if and only if they are equal (in the type-theoretic sense).

  2. Any category can be turned into a univalent category via a universal construction, which we call the Rezk completion.

10 février 2014, 14:00 : Séminaire

Giuseppe Greco (Delft University of Technology), Proof theory for dynamic logics

We introduce a multi-type display calculus for (intuitionistic) dynamic epistemic logic and (concurrent) propositional dynamic logic, which we refer to as Dynamic Calculi. The display approach is suitable to modularly chart the space of dynamic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculi with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems that enjoy a generalisation of the Curry-Belnap cut-elimination meta-theorem.

16 janvier 2014, 11:00 : Séminaire

Alberto Carraro (Università Ca' Foscari, Venise), Semantical analysis of λ-calculus by (Differential) Linear Logic

We present some results about the relational semantics of λ-calculus. The standard relational semantics satisfies the so-called Taylor expansion formula and this forces all models of untyped λ-calculus in it to be sensible. We illustrate a model, obtained by modifying the exponential modality, in which the Taylor formula does not hold, allowing the existence of a non-sensible relational model. For a model in the standard semantics we illustrate a syntax in which all points are definable, leading to a full abstraction result. We then move our attention to call-by-value λ-calculus in the relational semantics. We characterize the solvable terms and we discuss the relationship between the equational theory of a model, Böhm trees, and operational equivalence. We will point out how all the ideas underlying these results come from (Differential) Linear Logic.