Damien Pous

CNRS researcher, in charge of the Plume team. (CNRS, ENS Lyon, LIP, UMR 5668) eMail: Damien dot Pous at ens-lyon dot fr Office: (+33) 4 72 72 82 30     M7 310, LIP, ENS Lyon 46 allée d'Italie 69364 Lyon Home: 47 rue Prof. Grignard 69007 Lyon Keywords Kleene algebra, automata, logic, bisimulation, pi, lambda, ccs, coalgebra, up-to techniques, Rocq

Circles

• By first names: Alan, Alexandra, Amina Anupam, Aurélien, Christian, Cyril, Daniel, Daniela, Davide, Denis, Enric, Filippo, Florent, Georg, Henning, Jean-Marie, Jana, Jurriaan, Laureline, Lukas, Olivier, Paul, Romain, Samoth, Samuel, Samuel, Thomas, Tom, Valeria.
• By last names: Arsac, Basold, Bonchi, Braibant, Bréhard, Brunet, Cosme-Llópez, Cohen, Das, Demangeon, Doczkal, Doumane, Gazagnaire, Hirschkoff, Hirschowitz, Humeau, Kuperberg, Laurent, Madiot, Mulder, Pardon, Petrisan, Pinault, Rot, Sangiorgi, Schmitt, Silva, Struth Vignudelli, Wagemaker.

Code

Formal proofs and libraries

• String diagrams for monoidal categories.
• Adhesive category theory in Rocq (with Samuel Arsac and Russ Harmer).
• Graph theory: K4-free = TW2 (Christian Doczkal and Guillaume Combette as main authors).
• Chebyshev rigorous approximations (with Florent Bréhard and Assia Mahboubi).
• Coinduction all the way up: a new library for -impredicative- coinduction in Coq.
• Relation Algebra and KAT in Coq (includes a tactic for deciding Kleene algebras with Tests).
• Certification of robust reconfiguration algorithms (joint work with Fabienne Boyer and Olivier Gruber).
• Algebraic Tools for Binary Relations (includes a tactic for deciding Kleene algebras---joint work with Thomas Braibant).
• Plugin for rewriting modulo associativity and commutativity (joint work with Thomas Braibant).
• Formalisation of the entire ICALP'05 article.
• Certified compiler from recursive functions to Minski machines.

Algorithms

• Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests (KAT).
• A new algorithm for NFA language equivalence.
• Checking must testing using bisimulations up to congruence.
• Optimised proof search algorithm for cyclic linear logic.

Abstract Machines

• Distributed implementation of an abstract machine for Safe Ambient.
• Graphical machine for interpreting various notions of Mobile Ambients in a funny way.

Teaching

• Assisted proofs (with Daria Pchelina, Nathalie Revol and Michale Rao, M2 ENS Lyon, 2025-2026)
• Type theory and Rocq (with Cyril Cohen, M2 maths avancées ENS Lyon, 2024-2025)
• Coalgebra (with Valeria Vignudelli, M2 ENS Lyon, 2023-2024, 2024-2025)
• Relation algebraic methods (with Amina Doumane and Georg Struth, M2 ENS Lyon, 2021-2022, 2022-2023)
• Coinduction and Coq (with Yannick Zakowski, M2 ENS Lyon, 2021-2022, 2022-2023)
• Certified Approximation (with Nicolas Brisebarre, M2 ENS Lyon, 2018-2019, 2020-2021, 2023-2024, 2024-2025)
• Automata, coinduction, and relation algebra (M2 ENS Lyon, 2017-2018)
• Mechanised Coinductive Proofs (with Daniel Hirschkoff and Jean-Marie Madiot, ECNU Shanghai, 2016)
• Coinductive methods (with Filippo Bonchi and Daniel Hirschkoff, M2 ENS Lyon, 2015-2016, 2016-2017)
• Mechanizing rational languages (EPIT research school, 2015)
• Techniques « up-to » et applications en algorithmique (Geocal research school, 2015)
• Coinduction, automata, coalgebra (with Filippo Bonchi, Pisa, 2015)
• Du lycée au CNRS, mathématiques et ordinateurs (exposé pour les Cordées de la réussite, au Puy-en-Velay, avril 2014)
• Floating point arithmetic and formal proofs (with Jean-Michel Muller and Laurent Théry, M2 ENS Lyon, 2012-2013, 2013-2014, 2016-2017)
• Coq: from theory to practice (EJCP research school, 2013)
• Concurrency theory and Implicit Complexity (with Patrick Baillot, M2 ENS Lyon, 2012-2013)
• First steps with Coq (for primary and secondary school teachers, APMEP, Grenoble, 2011)
• Coq: from theory to practice (with Alan Schmitt, MSTII, UJF Grenoble, 2011).
• Bisimulations and process calculi (with Alan Schmitt, MSTII, UJF Grenoble, 2010).
• Natural deduction (DLST, UJF Grenoble, 2010, 2011).
• Functional programming (lambda-calculus, OCaml) (ENS Lyon, 2005-2006, 2006-2007).
• Logic, semantics and rewriting theory (ENS Lyon, 2005-2006, 2006-2007, 2007-2008).
• Computer assisted proofs (Coq) (ENS Lyon, 2007-2008).

CoVeCe

A project funded by the ERC, about Coinduction for Verification and Certification.

Publications: HAL, dblp, gg.scholar

Most articles are freely available from HAL, sometimes with a few additional details or proofs w.r.t. the published version. Please drop me an email if you can't find one.

Personal Page

Nouveau: pour connaître mon indice de Pous, demandez à Romain Demangeon.