Groupe de travail

Unless otherwise stated, talks are held on Mondays at 2pm in room 315 on the 3rd floor of the M7 building. Contact Matteo Mio (matteo.mio@ens-lyon.fr) or Denis Kuperberg (denis.kuperberg@ens-lyon.fr) to organize a talk.

Upcoming talks

  • 24/06/2019 : Quentin Peyras. Propriété du domaine borné pour un fragment pratique de la logique linéaire temporelle du premier ordre

Previous talks

2018/19

  • 17/06/2019 : Jan Martens. Resynchronizability of one-way transducers is undecidable
  • 20/05/2019 : Pierre Lescanne. A lambda calculus with explicit duplication, explicit erasure and implicit names
  • 2/05/2019 : Paul-Elliott Angles d’Auriac. Arithmetic transfinite recursion and the Axiom of Choice
  • 25/04/2019 : Filippo Bonchi. Graphical conjunctive queries
  • 15/04/2019 : Valeria Vignudelli. The theory of traces for systems with nondeterminism and probability
  • 8/04/2019 : Lorenzo Tortora de Falco. On some uses of connectedness in linear logic
  • 1/04/2019 : Eugenia Oshurko. Knowledge representation and update in hierarchies of graphs
  • 28/03/2019 : Olivier Carton. Normal numbers with constraints
  • 25/03/2019 : Henning Basold. Recursive proofs for the mu-calculus – with and without probabilities
  • 18/03/2019 : Pierre Pradic. A Dialectica-like interpretation of a linear MSO on infinite words
  • 11/03/2019 : Tom Hirschowitz. Simple game semantics and Day convolution
  • 4/03/2019 : Laureline Pinault. Extension of LKA with structural rules
  • 11/02/2019 : Denis Kuperberg. Bouncing threads for infinitary and circular proofs
  • 4/02/2019 : Olivier Laurent. Formalizing quantifiers
  • 28/01/2019 : Pierre Pradic. Non-constructiveness of the Cantor-Bernstein theorem
  • 6/12/2018 : Alexis Ghyselen. Type-based complexity analysis of probabilistic functional programs
  • 29/11/2018 : Fabian Reiter. Descriptive distributed complexity
  • 22/11/2018 : Matteo Mio & Christophe Lucas. A hyper-sequent calculus for a probabilistic modal logic
  • 8/11/2018 : Peio Borthelle. Ornaments and induction-recursion
  • 25/10/2018 : Marc de Visme. Quantum game semantics
  • 11/10/2018 : Pierre Clairambault. Linearity in higher-order recursion schemes
  • 27/09/2018 : Marc Bagnol. Büchi Good-for-Games automata are recognizable in PTime
  • 24/09/2018 : Mahsa Shirmohammadi. On rationality of non-negative matrix factorization

2017/18

  • 3/07/2018 : Marc de Visme. A definable game semantics for the linear quantum lambda-calculus
  • 2/07/2018 : Aurore Alcolei. Resource-tracking concurrent games
  • 25/06/2018 : Valeria Vignudelli. Proof techniques for program equivalence in probabilistic
    higher-order languages
  • 18/06/2018 : Stefania Dumbrava. Certified graph view maintenance with regular Datalog
  • 7/06/2018 : Andrzej Murawski. Higher-order linearisability
  • 14/05/2018 : Adrien Durier. Open call-by-value and the pi-calculus
  • 24/04/2018 : Gabriel Scherer. Tout réussir en répétant beaucoup
  • 23/04/2018 : Laure Daviaud. When is containment decidable for probabilistic automata?
  • 9/04/2018 : Marc de Visme. Quantum Game Semantics
  • 26/03/2018 : Simon Iosti. The synthesis of eventually safe properties via Good-for-Games automata
  • 19/03/2018 : Christian Doczkal. A formal proof of the graph minor theorem for treewidth 2
  • 5/03/2018: Valia Mitsou. Limitations of treewidth for problems beyond NP
  • 26/02/2018 : Damien Pous. Non-well-founded proof theory for IMALL with lists
  • 12/02/2018 : Pierre Pradic. A Curry-Howard approach to Church’s synthesis via linear logic
  • 5/02/2018 : Henning Basold. Breaking the loop: recursive proofs for coinductive predicates in fibrations
  • 18/12/2017 : Filippo BonchiSound up-to techniques and complete abstract domain
  • 11/12/2017 : Sergueï Lenglet. Fully abstract encodings of lambda-calculus in HO-core through abstract machines
  • 4/12/2017 : Guilhem Jaber. A trace semantics for System F parametric polymorphism
  • 27/11/2017 : Luc Pellissier. PhD defense rehearsal
  • 16/10/2017 : Henning Basold. A recursive logic for the equivalence of inductive-coinductive programs
  • 9/10/2017 : Henryk Michalewski.  AlphaMath
  • 2/10/2017 : Amina Doumane.  Constructive completeness for the linear-time mu-calculus
  • 26/09/2017 : Olivier Laurent. Double-negations and focusing
  • 21/09/2017 : Jim Laird. Extensional and intensional semantics of bounded and unbounded nondeterminism

2016/17

  • 3/07/2017 : Simon Castellan. PhD defense rehearsal
  • 15/06/2017 : Vincent Michielini, Eugenia Oshurko & Laureline Pinault. M2 defence rehearsals
  • 29/05/2017 : Enric Cosme Llópez. On recognizability of graphs of bounded treewidth
  • 22/05/2017 : Anupam Das. From focused systems to complexity bounds
  • 18/04/2017 : Alessio Guglielmi. Decoupling normalization mechanisms with an eye towards concurrency
  • 10/04/2017 : Aurore Alcolei. A compositional proof of Herband’s Theorem through game semantics
  • 3/04/2017 : Anupam Das. Monotonicity in logic and complexity
  • 27/03/2017 : Olivier Laurent Linear logic, double-negation translations and expressiveness
  • 6/03/2017: Matteo Mio. An introduction to the duality theory of Boolean algebras with operators
  • 13/02/2017 : Pierre Pradic. Devising a realizability notion for Church’s synthesis
  • 6/02/2017 :  Simon Castellan. Non-angelic concurrent game semantics
  • 2/02/2017 : Alexandre Miquel. Implicative algebras: a new foundation for realizabity and forcing
  • 30/01/2017 : Valeria Vignudelli. Environmental bisimulations for probabilistic higher-order languages
  • 16/01/2017 : Chung-Kil Hur. A promising semantics for relaxed-memory concurrency
  • 12/12/2016 : Enric Cosme Llópez. A complete axiomatization of isomorphism of treewidth 2 graphs, part 2
  • 5/12/2016 : Enric Cosme Llópez. A complete axiomatization of isomorphism of treewidth 2 graphs, part 1
  • 17/11/2016 : Radu Mardare. Quantitative algebraic reasoning: towards a quantitative theory of effects
  • 17/10/2016 : Frédéric Prost. Attributed graph rewriting with sub-structure cloning
  • 10/10/2016 : Yves-Stan Le Cornec. Model checking de systèmes modulaires à l’aide de réductions hiérarchiques
  • 6/10/2016 : Georg Struth. Concurrent Kleene algebras and pomset languages
  • 3/10/2016 : Paul Brunet. Algebras of relations: from algorithms to formal proofs
  • 29/09/2016 : Peter Jipsen. Concurrent Kleene algebras with tests as algebraic models for concurrent programs
  • 26/09/2016 : Matias David Lee. Bisimulation over open terms for stream systems
  • 19/09/2016 : Damien Pous. Coinduction all the way up

2015/16

  • 27/06/2016 : Christian Doczkal. Informative completeness for decidable modal logics
  • 20/06/2016 : Russ Harmer. Implicit state simulation, part 2
  • 13/06/2016 : Russ Harmer. Implicit state simulation, part 1
  • 6/06/2016 : Anupam Das. Free-cut elimination in linear logic and an application to a feasible arithmetic
  • 30/05/2016 : Emmanuel Beffara. Proof-theoretical investigations in operational semantics, part 2
  • 23/05/2016 : Anupam Das. Linear rewriting systems for Boolean structures, part 2
  • 19/05/2016 : Anupam Das. Linear rewriting systems for Boolean structures, part 1
  • 9/05/2016 : Emmanuel Beffara. Proof-theoretical investigations in operational semantics, part 1
  • 2/05/2016 : Enric Cosme Llópez. Formations of monoids, congruences, and formal languages
  • 25/04/2016 : Enric Cosme Llópez. The dual equivalence of equations and co-equations for automata
  • 4/04/2016 : Frédéric Prost. Parallelism in AGREE transformations
  • 24/03/2016 : Jim Laird. Game semantics for bounded polymorphism
  • 21/03/2016 : Dominique Duval. Decorated semantics for an imperative language with exceptions
  • 14/03/2016 : Colin Riba. Categories of tree automata, part 2
  • 7/03/2016 : Colin Riba. Categories of tree automata, part 1
  • 3/03/2016 : Daniel Leivant. Syntax directed reasoning in dynamic logic: a coinductive approach
  • 29/02/2016 : Simon Castellan. Weak memory models using event structures.
  • 8/02/2016 : Damien Pous. Coinduction for Verification and Certification: an overview
  • 1/02/2016 : Filippo Bonchi. Rewriting string diagrams via DPO
  • 25/01/2016 : Laure Gonnord. An encoding of array verification problems into array-free Horn clauses
  • 11/01/2016 : Ugo Dal Lago. Particles vs. waves: is multiplicity really necessary?
  • 14/12/2015 : Pierre Clairambault. Relating causal and interleaving concurrent game semantics
  • 7/12/2015 : Matteo Mio. Regular sets of trees and probability
  • 30/11/2015 : Laure Daviaud. A gentle introduction to the profinite theory of rational languages, part 2
  • 26/11/2015 : Luigi Santocanale. Fixed-point elimination in the intuitionistic propositional calculus
  • 23/11/2015 : Jurriaan Rot. Coalgebraic trace semantics via forgetful logics
  • 19/11/2015 : Denis Kuperberg. Good-for-Games automata versus deterministic automata
  • 16/11/2015 : Laure Daviaud. A gentle introduction to the profinite theory of rational languages, part 1
  • 12/11/2015 : Maciej Bendkowski & Katarzyna Grygiel. Lambda terms and their combinatorial representations
  • 9/11/2015 : Jérôme Feret. An algebraic approach for inferring and using symmetries in rule-based models
  • 2/11/2015 : Matias David Lee. Logical characterization of bisimulation for transition relations over probability distributions with internal actions
  • 19/10/2015 : Adrien Basso-Blandin. A knowledge representation meta-model for rule-based modelling of signalling networks
  • 21/09/2015 : Olivier Laurent. Introduction à la focalisation et application à l’orthologique

2014/15

  • 15/06/2015 : Daniel Leivant. The computational contents of ramified co-recurrence
  • 18/05/2015 : Hélène Coullon. Towards component-based high performance computing
  • 11/05/2015 : Emmanuel Beffara. Vers l’unification des systèmes de types pour processus mobiles
  • 4/05/2015 : Frédéric Prost. Social data anonymisation and graph transformations
  • 27/04/2015 : Laure Gonnord. Validation of memory accesses through symbolic analyses
  • 20/04/2015 : Paul Brunet. A Kleene theorem for Petri automata
  • 2/04/2015 : Emmanuel Coquery. RQL: un langage “à la SQL” pour découvrir des règles à partir des données
  • 30/03/2015 : Patrick Baillot. Analyse de complexité par typage et réductions cryptographiques
  • 16/03/2015 : Anupam Das. No complete linear term rewriting for propositional logic (probably)
  • 9/03/2015 : Colin Riba. Representation of functions in second-order arithmetic and Girard’s System F
  • 5/03/2015 : Laure Daviaud. Max-plus automata and size-change abstraction
  • 2/03/2015 : Russ Harmer. Executable Knowledge
  • 23/02/2015 : Damien Pous. Kozen’s proof of completeness for Kleene algebra
  • 26/01/2015 : Pierre Clairambault. Introduction to normalization by evaluation
  • 19/01/2015 : Olivier Laurent. Small Problems Related with Provability in Linear Logic
  • 12/01/2015 : Alexandra Silva. Automata Learning: A Categorical Perspective
  • 5/01/2015 : Adrien Basso-Blandin. Conception d’un langage dédié à la conception de fonctions biologiques de synthèse par compilation de spécifications comportementales
  • 8/12/2014 : Matteo Mio. An overview of monadic second order logic (MSO)
  • 1/12/2014 : Pierre Clairambault. Game semantics and normalization by evaluation
  • 24/11/2014 : Philippe Audebaud. Ciao Scott. Benvenuto Zariski
  • 12/11/2014 : Jim Laird. Quantitative semantics for mobility
  • 3/11/2014 : Simon Castellan. La strategie de la fourchette
  • 13/10/2014 : Anupam Das. Some developments on the linear fragment of classical propositional logic
  • 06/10/2014 : Fabio Zanasi. How to kill epsilons with a dagger – a coalgebraic take on systems with algebraic label structure
  • 29/09/2014 : Paul Brunet. Decidability of identity-free relational Kleene lattices
  •  22/09/2014 : Emmanuel Beffara. Proofs as schedules
  • 15/09/2014 : Frédéric Prost. Graph Transformations : cloning issues

2014

  • 10/07/2014 : Ryan Kavanagh.  Coupled logical bisimulations for the lambda-calculus
  • 7/07/2014 : Anupam Das. On the pigeonhole and related principles in deep inference and monotone systems
  • 2/06/2014 : Jean-Marie Madiot. Bisimulations up-to: beyond first-order transition systems
  • 22/05/2014 : Denis Kuperberg. The theory of regular cost functions, from finite words to infinite trees
  • 19/05/2014 : Olivier Laurent. From Coq through System F to linear logic (the theory of l2coq) [S1E3]
  • 15/05/2014 : Simona Ronchi Della Rocca. Intersection types, inhabitation and solvability
  • 24/04/2014 : Valentin Blot. Realizability for classical analysis in a reference-enabled setting [S1E2]
  • 17/04/2014 : Olivier Laurent. From Coq through System F to linear logic (the theory of l2coq) [S1E2]
  • 31/03/2014 : Erika De Benedetti. Elementary lambda-calculus for a polyvalent characterization of k-(F)EXP
  • 27/03/2014 : Matthieu Perrinel. Stratified nested linear logic: passage des critères sémantiques à un système de type
  • 17/03/2014 : Valentin Blot. Realizability for classical analysis in a reference-enabled setting [S1E1]
  • 24/02/2014 : Olivier Laurent. From Coq through System F to linear logic (the theory of l2coq) [S1E1]
  • 20/02/2014 : Pierre-Evariste Dagand. Writing and verifying x86 assembly code in the Coq proof assistant
  • 17/02/2014 : Filippo Bonchi & Daniela Petrisan. Co-induction up-to in a fibrational setting
  • 27/01/2014 : Matteo Sammartino. An introduction to pre-sheaf models for nominal calculi
  • 9/01/2014 : Thomas Powell. Bar recursive extensions of Gödel’s system T
  • 6/01/2014 : Daniela Petrisan. Bi-simulation up-to in a fibrational setting