Our seminars are usually on Thursdays. Some of them are shared with the LIMD team of the LAMA laboratory, and are located in Chambéry. About once a month, the seminar is held as a CHoCoLa meeting.

Next Events

• Thursday 20th June, 10:30 am, room B2:
  Igor Walukiewicz (LaBRI).
  Transfer theorem
  (joint work with Sylvain Salvati)
  
  We consider simply-typed lambda calculus with fixpoint operators. Evaluation of a term gives as a result the Böhm tree of the term. We show that evaluation is compatible with monadic second-order logic (MSOL). This means that for a fixed finite vocabulary of terms, the MSOL properties of Böhm trees of terms are effectively MSOL properties of terms themselves. Theorems of this kind have been known for some graph operations: unfolding, and Muchnik iteration.
  Similarly to those results, our main theorem has diverse applications. It can be used to show decidability results, to construct classes of graphs with decidable MSOL theory, or to obtain MSOL formulas expressing behavioral properties of terms. Another application is decidability of a control-flow synthesis problem.

Past Events (since September 2010)

Since January 2013

• Thursday 30th May:
  Gabriel Scherer (Inria Gallium).
  Does a given type have a unique inhabitant? A work in progress.

• Thursday 23rd May:
  Bruno Salvy (Inria & LIP).
  Une introduction à la théorie des espèces de structures

• Friday 17th May:
  One day on circular proofs and fixed point logics
  Lutz Schroeder (joint work with Yde Venema):
  Flat coalgebraic fixed point logics
  Fabio Zanasi (joint work with Alessandro Facchini and Yde Venema):
  A characterization theorem for the alternation-free fragment of the modal mu-calculus
  Luigi Santocanale (joint work with Jérôme Fortier):
  La règle de coupure dans les preuves circulaires

• Thursday 16th May:
  CHoCoLa meeting

• Thursday 11th April:
  CHoCoLa meeting

• Thursday 14th March:
  CHoCoLa meeting

• Friday 22nd February:
  Thomas Colcombet (LIAFA, Paris).
  The use of monoids in formal language theory and Schützenberger's theorem.

• Thursday 21st February:
  Alejandro Díaz-Caro (Université Paris-Ouest & Inria Paris-Rocquencourt).
  Non-determinism (and probabilities) through type isomophism.

• Thursday 14th February:
  CHoCoLa meeting

• Thursday 7th February:
  Cyril Cohen (Gothenburg, Sweden).
  Formalization of algebraic numbers in Coq.

Since January 2011

• Tuesday 11th December:
  Thibaut Balabonski (Gallium, Inria Rocquencourt).
  La pleine paresse, une certaine optimalité.

• Monday 10th December:
  Daniela Petrisan (Leicester, UK).
  TBA

• Thursday 6th December:
  CHoCoLa meeting in Paris

• Monday 3rd December:
  Matteo Mio (LIX)
  Tree Games

• Thursday 15th November:
  CHoCoLa meeting

• Thursday 8th November:
  Luca Roversi (Torino University, Italy).
  Communication, and concurrency with restriction inside Deep-inference.

• Monday 5th November:
  Gilles Barthe (IMDEA Software Institute, Madrid)
  Computer-Aided Cryptographic Proofs and Designs

• Thursday 11th October:
  CHoCoLa meeting

• Thursday 4th October:
  Barbara Koenig (Univeristät Duisburg-Essen, Germany)
  Conditional Reactive Systems.

• Tuesday 2nd October:
  Russ Harmer (PPS)
  Constraining rule-based dynamics with types.

• Thursday 18th January:
  Frédéric Prost (CAPP, LIG, Grenoble)
  Enforcing Dynamic Interference Policy.

• Tuesday 6th September:
  Ichiro Hasuo (Dept. of Computer Science, University of Tokyo)
  Semantics of Higher-Order Quantum Computation via Geometry of Interaction
  (joint work with Naohiko Hoshino, RIMS, Kyoto University).

• Thursday 30th June:
  Stefan Hetzl (PPS)
  First-Order Proofs as Tree Languages

• Monday 30th May:
  Daniel Leivant (Indiana University (USA) & Loria (Nancy))
  The Comprehension Cube

• Thursday 19th May:
  Marcello Bonsangue (CWI, Amsterdam)
  Three coalgebraic characterizations of context free languages
  (joint work with J. Rutten and J. Winter).

• Wednesday 18th May:
  
  CoGip meets CWI
  • Damien Pous (CNRS, SARDES, LIG)
    A Tutorial on Bisimulation Up-To
  
  
  • Filippo Bonchi (CNRS, PLUME, LIP) & Jan Rutten (CWI, Amsterdam)
    A Coalgebraic Perspective on Linear Weighted Automata
    Filippo Bonchi: part 1 ; Jan Rutten: part 2.
  
  
  • Alexandra Silva (CWI, Amsterdam)
    Sound and complete axiomatizations of coalgebraic language equivalence

• Thursday 21st April:
  Lionel Nguyen Van Thé (LATP, Marseille)
  (LIMD seminar).

• Thursday 14th April:
  Tom Hirschowitz (LIMD, LAMA)
  (LIMD seminar).

• From Monday 4th to Thursday 7th April:
  
  Choco Party & Differential Linear Logic course
  Final meeting of the Choco ANR project.

• Thursday 31th March:
  Peter G. Hancock (University of Strathclyde, UK)
  (LIMD seminar).

• Thursday 17th March:
  Jacques Duparc (Université de Lausanne).
  Games to Look into (Topological) Complexity.
  An Application to Automata Theory: The Wagner Hierarchy

• Thursday 10th March:
  Xavier Urbain (ENSIIE & CEDRIC, CNAM).
  
  Démonstration automatique : techniques, outils et certification

• Thursday 3rd March:
  Arnaud Carayol (IGM, Université Paris Est & CNRS).
  
  Structures defined by higher-order recursion schemes

• Thursday 24th February:
  Federico Aschieri (Torino University, Italy).
  
  Classical Logic, Learning and Realizability

• Monday 21st February:
  Masahiro Hamano (PRESTO, Japan Science and Technology Agency (JST))
  
  A Geometry of Interaction for Polarized Linear Logic

• From Monday 14th February to Friday 18th February:
  
  Rule-based modelling and application to biomolecular networks
  (winter school ER 06 of the Computer Science Department).

• Thursday 10th February:
  Jacques Jayez (L2C2, Lyon)
  
  Projection, attachement et logique épistémique

• From Monday 31st January to Friday 4th February:
  
  Separation logics and applications
  (winter school ER 04 of the Computer Science Department).

• Thursday 27th January:
  Choco seminar.

• Thursday 20th January:
  Pierre Hyvernat (LIMD, LAMA)
  (LIMD seminar).

• Monday 17th January:
  Ugo Dal Lago (Université de Bologne & INRIA Sophia Antipolis)
  
  Linear Dependent Types and Relative Completeness.

• Thursday 13th January:
  Thomas Seiller (IML, Marseille)
  (LIMD seminar).

• Thursday 6th January:
  Danko Ilik,
  Constructive proofs of completeness, extra-intuitionistic principles, and delimited control operators
  [slides].

Since September 2010

• Thursday 9th December:
  Choco seminar.

• Thursday 25th November:
  Sylvain Salvati (INRIA Bordeaux Sud-Ouest & LaBRI),
  Extending Recognizability to the Simply Typed lambda-Calculus.

• Friday 19th November:
  Seminar of the COMPLICE ANR project.

• Thursday 18th November:
  Denis Cousineau (MSR-INRIA),
  An algebraic view of reducibility candidates.

• Wednesday 10th November:
  Jean-Louis Krivine (PPS, Paris 7),
  New models of ZF
  [slides].

• Thursday 4th November:
  Choco seminar.

• Tuesday 26th Ocotber:
  Ulrich Berger (Swansea),
  Program extraction from proofs using induction and coinduction.

• Thursday 21fst October:
  Giulio Manzonetto (Nijmegen),
  Full Abstraction for Resource Calculus with Tests.

• Thursday 7th October:
  Choco seminar.

• Friday 1st October:
  Amir Ben Amram (Tel-Aviv),
  An Introduction to Size-Change Termination Analysis
  (join seminar with the Compsys team).

• Thursday 16th September:
  Tom Hirschowitz (LIMD, LAMA),
  Cartesian closed 2-categories and higher-order rewriting
  (LIMD seminar).

• Tuesday 7th September:
  Jean-Yves Girard (IML, Marseille),
  La Normativité Logique.