Groupe de travail – PLUME: Programs & Proofs

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

8/04/2024 : Corentin Barloy. Circuit complexity of regular languages

Previous talks

2023/24

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ũng. A 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 Sarkis. Universal 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 Mazza. A 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 Bonchi. Sound 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