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 Amina Doumane (amina.doumane@ens-lyon.fr) or Valeria Vignudelli (valeria.vignudelli@ens-lyon.fr) to organise a talk.

Upcoming talks

  • 24/06/2024 : Rémi Di Guardia. Autour du théorème de Yeo

Previous talks

2023/24

  • 10/06/2024 : Samuel Arsac. The Raft consensus algorithm
  • 3/06/2024 : Nguyễn Lê Thành Dũng. Computing the polynomial degree of size-to-height increase for macro tree transducers
  • 27/05/2024 : Samuel Humeau. A finite presentation of graphs of treewidth at most three
  • 8/04/2024 : Corentin Barloy. Circuit complexity of regular languages
  • 22/01/2024 : Ralph Sarkis. Generalized_Metric_Spaces_Final_v3 (1)_Finla_DONE (2)
  • 15/01/2024 : Jérémie Marquès. A duality between theories of linear orders and a class of profinite monoids
  • 11/12/2023 : Denis Kuperberg. SMT Solving and modelling for biology
  • 4/12/2023 : Paolo Pistone. Tropical mathematics and the lambda calculus
  • 13/11/2023 : Nathan Lhote. Minimization of Cost Register Automata over a field
  • 6/11/2023 : Cyril Cohen. Unsolvability of the Quintic formalized in dependent type theory
  • 9/10/2023 : Samuel Arsac. Verification using the Conditional Contextual Refinement framework
  • 5/10/2023 : Paolo Torrini. Support for enriched categories in Hierarchy Builder
  • 2/10/2023 : Nguyễn Lê Thành Dũng. Algebraic recognition of regular functions
  • 25/09/2023 : Michele Pagani. The variable elimination algorithm as a let-term rewriting
  • 18/09/2023 : Cyril Cohen. Hierarchy Builder, a language and tool for designing and maintaining algebraic hierarchies

2022/23

  • 10/07/2023 :
    • Galaad Langlois. (Co)datatypes in Coq via W-types and M-types in the category of setoids
    • Pierre Goutagny. Kleene algebra with hypotheses: modular formalisation
  • 19/06/2023 : Dakotah Lambert. Algebraic perspectives on words and their parts
  • 22/05/2023 : Nguyễn Lê Thành Dũng. Unique perfect matchings and proof nets
  • 15/05/2023 : Rémi Di Guardia. A simple proof of sequentialization for MLL proof nets
  • 24/04/2023 : Sam van Gool. Modal unification and graph homomorphisms
  • 20/03/2023 : Nguyễn Lê Thành DũngA complexity gap between pomset logic and system BV
  • 13/03/2023 : Nguyễn Lê Thành Dũng. Polyregular functions: some recent developments
  • 6/03/2023 : Ralph SarkisUniversal relational algebra (with string diagrams)
  • 27/02/2023 : Wesley Fussner. Interpolation in semilinear logics
  • 20/02/2023 : Paweł Parys. The probabilistic Rabin tree theorem
  • 30/01/2023 : Ralph Sarkis. Diagrammatic reasoning for the category Rel
  • 23/01/2023 : Olivier Idir. Automates explorables : expressivité et décidabilité
  • 12/12/2022 : Ambroise Lafont. Generic pattern unification: a categorical approach
  • 5/12/2022 : Alexandre Goy. Weakening distributive laws using string diagrams
  • 28/11/2022 : Colin Riba. Locally finitely presentable arboreal adjunctions
  • 21/11/2022 : Damiano MazzaA categorical approach to descriptive complexity theory
  • 7/11/2022 : Rémi Di Guardia. Type isomorphisms for Multiplicative-Additive Linear Logic, part II
  • 24/10/2022 : Nguyễn Lê Thành Dũng. Aperiodicity in a non-commutative logic, part II
  • 17/10/2022 : Nguyễn Lê Thành Dũng. Aperiodicity in a non-commutative logic
  • 10/10/2022 : Rémi Di Guardia. Type isomorphisms for Multiplicative-Additive Linear Logic
  • 3/10/2022 : Alexandre Fernandez. Synchronous and non-deterministic spatial computations with global transformations
  • 26/09/2022 : Damien Pous. Reductions for Kleene algebra with top

2021/22

  • 27/06/2022 : Émile Hazard. Explorable automata: let’s play with some tokens!
  • 23/05/2022 : Ralph Sarkis. Quantitative algebraic reasoning : Our recent breakthrough and the bigger picture
  • 13/12/2021 : Kenji Maillard. Models of CIC for gradual dependent types [visio]
  • 06/12/2021 : Pierre Lescanne. Almost all classical propositions are intuitionistic — Zaionc paradox revisited
  • 30/11/2021 : Leo Exibard. Reactive synthesis over infinite data domains with machines with registers
  • 29/11/2021 : Leo Stefanesco. An asynchronous soundness theorem for concurrent separation logic
  • 22/11/2021 : Pierre Ohlmann. Positionalité pour un joueur dans les jeux à durée infinie
  • 15/11/2021 : Tom Hirschowitz. Initial-algebra semantics with inductive auxiliary operations [visio]
  • 8/11/2021 : Alexandre Goy. A journey from alternation to non-determinism on the back of distributive laws
  • 25/10/2021 : Christophe Lucas. Free modal Riesz spaces are Archimedean: a syntactic proof
  • 18/10/2021 : Ambroise Lafont. Variable binding and substitution for (nameless) dummies
  • 11/10/2021 : Théo Winterhalter. Metacoq and rewrite rules, formally verified meta-theory
  • 4/10/2021 : Ralph Sarkis. Quotienting a monad via projective algebras

2020/21 [visio]

  • 7/06/2021 : Luca Reggio. Arboreal categories: an axiomatic theory of resources
  • 31/05/2021 : Lison Blondeau-Patissier. Positional injectivity for innocent strategies
  • 10/05/2021 : Étienne Miquey. Evidenced frames: a unifying framework broadening realizability models
  • 12/04/2021 : Ralph Sarkis. Combining nondeterminism, probability, and termination: equational and metric reasoning
  • 22/03/2021 : Christophe Lucas. Proof theory of modal Riesz spaces
  • 8/03/2021 : Pierre Pradic. Implicit automata in λ-calculi
  • 15/02/2021 : Davide Barbarossa. Qualitative Taylor expansion for lambda-mu-calculus with some applications
  • 8/02/2021 : Alexis Ghyselen. Types for parallel complexity of pi-calculus processes
  • 25/01/2021 : Raphaëlle Crubillé. On higher-order cryptography
  • 14/12/2020 : Denis Kuperberg. Positive first-order logic on words

2019/20

  • 24/02/2020 : Emile Hazard. Proof systems for the inclusion of languages of infinite words
  • 10/02/2020 : Udi Boker. Why these automata types?
  • 3/02/2020 : Michał Skrzypczak. Computing measures of weak-MSO definable sets of trees
  • 27/01/2020 : Alexis Ghyselen. Causal complexity in pi-calculus
  • 16/12/2019 : Luca Reggio. Duality and limits of finite structures
  • 3/12/2019 : Alex Simpson. Sheaf-theoretic principles for reasoning about independence
  • 4/11/2019 : Colin Riba. Temporal refinements for guarded recursive types
  • 21/10/2019 : Karoliina Lehtinen. Quasi-polynomial techniques for parity games and other problems
  • 7/10/2019 : Damien Pous. A certificate-based approach to formally verified approximations
  • 30/09/2019 : Alexis Ghyselen. Parallel complexity with types in a process calculus
  • 23/09/2019 : Olivier Laurent. Phase semantics for cut elimination
  • 2/09/2019 : Christian Doczkal. Graph theory in Coq: minors, treewidth and isomorphisms

Archive (01/2014–06/2019)

2018/19

  • 24/06/2019 : Quentin Peyras. Propriété du domaine borné pour un fragment pratique de la logique linéaire temporelle du premier ordre
  • 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