| 2026 | CONCUR | Continuous Algebras with Hypotheses. | Lukas Mulder, Damien Pous, Jana Wagemaker |
| 2026 | CPP | Adhesive Category Theory for Graph Rewriting in Rocq. | Samuel Arsac, Russ Harmer, Damien Pous |
| 2026 | ITP | String Diagrams for Monoidal Categories, in Rocq. | Damien Pous |
| 2026 | MFCS | Diagrammatic Reasoning, Formally (Invited Talk). | Damien Pous |
| 2024 | ICALP | A Finite Presentation of Graphs of Treewidth at Most Three. | Amina Doumane, Samuel Humeau, Damien Pous |
| 2022 | CONCUR | Completeness Theorems for Kleene Algebra with Top. | Damien Pous, Jana Wagemaker |
| 2020 | CONCUR | Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms. | Amina Doumane, Damien Pous |
| 2020 | CPP | Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. | Christian Doczkal, Damien Pous |
| 2019 | CALCO | Coinduction: Automata, Formal Proof, Companions (Invited Paper). | Damien Pous |
| 2019 | DLT | Coinductive Algorithms for Bchi Automata. | Denis Kuperberg, Laureline Pinault, Damien Pous |
| 2019 | FOSSACS | Kleene Algebra with Hypotheses. | Amina Doumane, Denis Kuperberg, Damien Pous, Ccilia Pradic |
| 2019 | ITP | A Certificate-Based Approach to Formally Verified Approximations. | Florent Brhard, Assia Mahboubi, Damien Pous |
| 2018 | CONCUR | Completeness for Identity-free Kleene Lattices. | Amina Doumane, Damien Pous |
| 2018 | CSL | Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices). | Anupam Das, Damien Pous |
| 2018 | ITP | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. | Christian Doczkal, Guillaume Combette, Damien Pous |
| 2018 | LICS | Allegories: decidability and graph homomorphisms. | Damien Pous, Valeria Vignudelli |
| 2018 | LPAR | Left-Handed Completeness for Kleene algebra, via Cyclic Proofs. | Anupam Das, Amina Doumane, Damien Pous |
| 2018 | MFCS | Treewidth-Two Graphs as a Free Algebra. | Christian Doczkal, Damien Pous |
| 2018 | STACS | On the Positive Calculus of Relations with Transitive Closure. | Damien Pous |
| 2017 | CALCO | Monoidal Company for Accessible Functors. | Henning Basold, Damien Pous, Jurriaan Rot |
| 2017 | CONCUR | On Decidability of Concurrent Kleene Algebra. | Paul Brunet, Damien Pous, Georg Struth |
| 2017 | FOSSACS | Companions, Codensity and Causality. | Damien Pous, Jurriaan Rot |
| 2017 | LICS | Fully abstract encodings of λ-calculus in HOcore through abstract machines. | Malgorzata Biernacka, Dariusz Biernacki, Sergue Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt |
| 2017 | MFCS | K4-free Graphs as a Free Algebra. | Enric Cosme-Llpez, Damien Pous |
| 2017 | TABLEAUX | A Cut-Free Cyclic Proof System for Kleene Algebra. | Anupam Das, Damien Pous |
| 2016 | ITP | Cardinalities of Finite Relations in Coq. | Paul Brunet, Damien Pous, Insa Stucke |
| 2016 | LICS | Coinduction All the Way Up. | Damien Pous |
| 2016 | MFCS | A Formal Exploration of Nominal Kleene Algebra. | Paul Brunet, Damien Pous |
| 2015 | CONCUR | Lax Bialgebras and Up-To Techniques for Weak Bisimulations. | Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot |
| 2015 | LICS | Petri Automata for Kleene Allegories. | Paul Brunet, Damien Pous |
| 2015 | POPL | Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. | Damien Pous |
| 2015 | POPL | Coinductive techniques, from automata to coalgebra. | Damien Pous |
| 2014 | CONCUR | Bisimulations Up-to: Beyond First-Order Transition Systems. | Jean-Marie Madiot, Damien Pous, Davide Sangiorgi |
| 2014 | CSL | Coinduction up-to in a fibrational setting. | Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot |
| 2013 | APLAS | Brzozowski's and Up-To Algorithms for Must Testing. | Filippo Bonchi, Georgiana Caltais, Damien Pous, Alexandra Silva |
| 2013 | CALCO | Coalgebraic Up-to Techniques. | Damien Pous |
| 2013 | ICSE | Robust reconfigurations of component assemblies. | Fabienne Boyer, Olivier Gruber, Damien Pous |
| 2013 | ITP | Kleene Algebra with Tests and Coq Tools for while Programs. | Damien Pous |
| 2013 | POPL | Checking NFA equivalence with bisimulations up to congruence. | Filippo Bonchi, Damien Pous |
| 2011 | CPP | Tactics for Reasoning Modulo AC in Coq. | Thomas Braibant, Damien Pous |
| 2010 | CSL | Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic. | Damien Pous |
| 2010 | ICALP | On Bisimilarity and Substitution in Presence of Replication. | Daniel Hirschkoff, Damien Pous |
| 2010 | ITP | An Efficient Coq Tactic for Deciding Kleene Algebras. | Thomas Braibant, Damien Pous |
| 2007 | APLAS | Complete Lattices and Up-To Techniques. | Damien Pous |
| 2007 | FOSSACS | A Distribution Law for CCS and a New Congruence Result for the | Daniel Hirschkoff, Damien Pous |
| 2006 | CONCUR | Weak Bisimulation Up to Elaboration. | Damien Pous |
| 2005 | Coordination | A Correct Abstract Machine for Safe Ambients. | Daniel Hirschkoff, Damien Pous, Davide Sangiorgi |
| 2005 | GPCE | Component-Oriented Programming with Sharing: Containment is Not Ownership. | Daniel Hirschkoff, Tom Hirschowitz, Damien Pous, Alan Schmitt, Jean-Bernard Stefani |
| 2005 | ICALP | Up-to Techniques for Weak Bisimulation. | Damien Pous |