17 décembre 2013

Séminaire à la FRIIAM à 14h: Sara Negri, Proofs and countermodels in labelled sequent calculi: some recent developments.

12 décembre 2013

Séminaire Chocola à Paris.

9 décembre 2013

Réunion Logoi à Paris.

21 novembre 2013, 14:00 : Groupe de travail

Répétition de soutenance de thèse.

Clément Aubert, Logique linéaire et classes de complexité sous-polynomiales

Cette recherche en informatique théorique construit de nouveaux ponts entre logique linéaire et théorie de la complexité. Elle propose deux modèles de machines abstraites qui permettent de capturer de nouvelles classes de complexité avec la logique linéaire, les classes des problèmes efficacement parallélisables (NC et AC) et celle des problèmes solutionnables a avec peu d’espace, dans ses versions déterministes et non-déterministes (L et NL). La représentation des preuves de la logique linéaire comme réseaux de preuves est employée pour représenter efficacement le calcul parallèle des circuits booléens, y compris à profondeur constante. La seconde étude s’inspire de la géométrie de l’interaction, une délicate reconstruction de la logique linéaire à l’aide d’opérateurs d’une algèbre de von Neumann. Nous détaillons comment l’interaction d’opérateurs représentant des entiers et d’opérateurs représentant des programmes peut être reconnue nilpotente en espace logarithmique. Nous montrons ensuite comment leur itération représente un calcul effectué par des machines à pointeurs que nous définissons et que nous rattachons à d’autres modèles plus classiques. Ces deux études permettent de capturer de façon implicite de nouvelles classes de complexité, en dessous du temps polynomial.

14 novembre 2013

Séminaire Chocola à Lyon:

  • Beniamino Accattoli (Bologne)
  • Dominic Hughes (Stanford)
  • Neelakantan R. Krishnaswami (Max Planck Institute)

22 octobre 2013

Colloquium de logique à la FRUMAM:

  • Laurent Regnier (Marseille), L'isomorphisme de Curry-Howard: les programmes sont-ils des démonstrations?
  • André Hirschowitz (Nice), Le printemps logique
  • Alain Prouté (Paris), Le formalisme Saunders

21 octobre 2013 : Soutenance de thèse

Soutenance de la thèse de Pierre Rannou, intitulée Réécriture de diagrammes et de Σ-diagrammes, à 14h dans l'amphi Herbrand.

17 octobre 2013

Séminaire Chocola à Lyon:

  • Aloïs Brunel (Univ. Paris 13), Composing forcing and classical realizability: the monitoring calculus
  • Guillaume Brunerie (Univ. Nice Sophia Antipolis), Homotopy type theory and homotopy groups of spheres
  • Matteo Mio (CWI, Amsterdam), Semantic Foundations of Quantitative (real-valued) Logics based on Functional Analysis

10 octobre 2013, 14:00 : Séminaire

Lionel Rieg (ENSIIE, Évry), L'interprétation calculatoire du forcing en réalisabilité classique : l'exemple des arbres de Herbrand

Jean-Louis Krivine a présenté en 2011 une méthode pour combiner le forcing de Cohen et la réalisabilité classique dans laquelle les conditions de forcing s'interprètent calculatoirement comme des références non soumises aux backtracks. Alexandre Miquel a reformulé la traduction de programme sous-jacente dans un cadre typé, l'arithmétique d'ordre supérieur (PAω⁺) et l'a intégré directement à la KAM, donnant la KFAM (Krivine's Forcing Abstract Machine).

Dans cet exposé, je vais donner les idées essentielles de cette transformation de programme issue du forcing et expliquer comment elle peut s'utiliser en pratique. J'illustrerai ensuite cette méthodologie par un exemple concret : la construction d'arbre de Herbrand.

26 septembre 2013

Séminaire Chocola à Lyon:

  • Michele Basaldella, An interactive semantics for classical proofs
  • Michele Pagani (LIPN, Univ. Paris 13), Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF
  • Christophe Raffalli (LAMA, Université de Savoie), Nullstellensatz and Positivestellensatz from cut-elimination

20 septembre 2013 : Séminaire de rentrée

10:00: Michele Basaldella, An interactive semantics for classical arithmethic

In this talk, we present a semantics of derivations for an infinitary logic introduced by Novikoff and later refined by Coquand and Herbelin. The language of this logic consists of infinitary propositional formulas, and the proof-system for this language is given by a sequent calculus with infinitary rules of inferences. First-order classical arithmetic can be naturally embedded in this logic. The semantics of derivations we develop in this paper is strongly inspired by Girard’s ludics. The main result of this paper is a soundness-and-completeness theorem for derivations in the infinitary logic with respect to this kind of semantics.

14:00: Clément Aubert, Proof circuits and parallel cut-elimination in logarithmic space

Terui, Mogbil and Rahli detailed how it was possible to compute Boolean functions in parallel with proof-nets for MLLu. We introduced Proof circuits to lighten the encoding of Boolean Circuits into proof-nets, extending previous results to sub-logarithmic classes of complexity. It happened that this way of constraining our proof-nets eased their simulation by Alternating Turing Machine, the most general kind of Turing Machine. We present a small extension to previous results, where proof-nets can be normalized with logarithmic space.

4 juin 2013, 10:30 : Groupe de travail

Marc Bagnol, Le critère de correction Mogbil-Naurois

V. Mogbil et P. Naurois ont établi que la correction des réseaux de preuves M(E)LL est NL-complète en introduisant un nouveau critère de correction, équivalent au critère de Danos-Regnier. J.-Y. Girard a repris l'idée de ce critère dans son dernier article (GdI6) sous le nom de « switchings virtuels », utilisés dans le critère de correction des modalités exponentielles.

Je vous parlerai du critère Mogbil-Naurois: définition, exemples, complexité... et (exclusif!) je donnerai une preuve directe et très simple de séquentialisation des réseaux MLL pour ce critère, sans passer par l'équivalence avec Danos-Regnier.

23 mai 2013, 14:00 : Séminaire

Séminaire commun avec l'équipe MoVe du LIF.

Jérôme Fortier, La règle de coupure dans les preuves circulaires

Les preuves circulaires, dans lesquelles certaines conclusions peuvent être démontrées à partir d’elles-mêmes, furent introduites dans [1] pour étudier la calculabilité dans les modèles du μ-calcul, soit avec les opérations suivantes : produits et coproduits finis, algèbres initiales et coalgèbres terminales. Le calcul en question, sans règle de coupure, était correct et complet, mais pas plein, c’est-à-dire qu’il ne représentait pas toute la structure des modèles catégoriques visés.

On remplit donc le système de preuves circulaires en introduisant la règle de coupure. La nouvelle syntaxe permet une procédure d’élimination des coupures qui produit un arbre infini, modélisant ainsi le calcul recherché.

Plusieurs directions de recherche en découlent, qui sauront, on l’espère, intéresser autant les logiciens que les informaticiens !

[1] L. Santocanale, A calculus of circular proofs and its categorical semantics, in : M. Nielsen, U. Engberg (eds.), FOSSACS 2002, No. 2303 in LNCS, Springer, 2002.

Du 23 avril au 13 juin 2013 : Groupe de travail

23 avril 2013

10:30: Robin Cockett (Calgary), Cours sur les catégories différentielles

25 avril 2013

10:30: Robin Cockett (Calgary), Cours sur les catégories différentielles

30 avril 2013

10:30: Robin Cockett (Calgary), Cours sur les catégories différentielles

2 mai 2013

14:00: Robin Cockett (Calgary), Cours sur les catégories différentielles

21 mai 2013

10:30: Robin Cockett (Calgary), Cours sur les catégories différentielles

23 mai 2013

10:30: Robin Cockett (Calgary), Cours sur les catégories différentielles

13 juin 2013

14:00: Robin Cockett (Calgary), Cours sur les catégories différentielles

21 mars 2013, 14:00 : Groupe de travail

Thomas Leventis, Incompleteness of classes of models of the λ-calculus

Through the study of particular models, the Lambda Abstraction Algebras, Antonino Salibra has found a completeness criterion for classes of algebraic models of the λ-calculus that none of the usual classes respect, thus proving their incompleteness. We will present this result, then show that the categorical class of models built from the reflexive objects in MRel is also incomplete.

7 mars 2013, 10:30 : Groupe de travail

Subashis Chakraborty (Calgary), The proof theory of message passing with protocols

Sequential programs are connected through the λ-calculus by the Curry-Howard-Lambek isomorphism to intuitionistic proofs and cartesian closed category. The Curry-Howard isomorphism allows proofs to be viewed as programs and propositions as types. But what is the proof theory of concurrent programs? Message passing is a key element of concurrent programming. In the paper The Logic of Message Passing (2007), Cockett and Pastro showed how message passing could be accomodated in the proof theoretic framework for concurrency. They used the two-sided proof theory of cut elimination and described a categorical semantics of the system. In this talk, we will describe this two-tier message passing logic. We will focus on providing an intuition for the system. The cut elimination of the system provides an operational semantics, which we shall illustrate with examples. We will also go through some examples to show how protocols work in this system, where protocols actually datatype in the process (concurrent) world.