Damien Pous
CNRS researcher, member of the
Plume team.
(LIP, ENS de Lyon, UMR 5668)
eMail:
Damien dot Pous at enslyon dot fr

Office: (+33) 4 26 23 39 32
GN1 Sud 337, LIP, ENS Lyon
46 allée d'Italie 69364 Lyon


Home: (+33)9 53 27 49 82
36 rue Chevreul 69007 Lyon

Keywords
Kleene algebra, automata, logic, bisimulation, pi, lambda, ccs, coalgebra,
upto techniques, Coq
Circles
 By first names:
Alan,
Alexandra,
Anupam,
Aurélien,
Christian
Daniel,
Daniela,
Davide,
Enric,
Filippo,
Florent,
JeanMarie,
Jurriaan,
Olivier,
Paul,
Romain,
Samoth,
Thomas,
Tom,
Valeria.
 By last names:
Bonchi,
Braibant,
Bréhard,
Brunet,
CosmeLlópez,
Das,
Demangeon,
Doczkal,
Gazagnaire,
Hirschkoff,
Hirschowitz,
Laurent,
Madiot,
Pardon,
Petrisan,
Rot,
Sangiorgi,
Schmitt,
Silva,
Vignudelli.
CoVeCe
Code
Formal proofs and libraries
Algorithms
Abstract Machines
Teaching
 Mechanised Coinductive Proofs (with
Daniel Hirschkoff and JeanMarie Madiot, ECNU Shanghai, 2016)
 Coinductive methods (with
Filippo Bonchi and Daniel Hirschkoff, M2 ENS Lyon, 20152016, 20162017)
 Mechanizing rational languages (EPIT research school, 2015)
 Techniques « upto » 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
PuyenVelay, avril 2014)
 Floating point arithmetic and formal proofs (with
JeanMichel Muller and Laurent Théry, M2 ENS Lyon, 20122013, 20132014, 20162017)
 Coq: from theory to practice (EJCP research school, 2013)
 Concurrency theory and Implicit Complexity (with Patrick
Baillot, M2 ENS Lyon, 20122013)
 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 (lambdacalculus, OCaml) (ENS Lyon, 20052006, 20062007).
 Logic, semantics and rewriting theory (ENS Lyon, 20052006, 20062007, 20072008).
 Computer assisted proofs (Coq) (ENS Lyon, 20072008).
Book chapter
In journals

A General Account of Coinduction Upto,
.pdf.
F. Bonchi, D. Petrisan, D. Pous, J. Rot,
Acta Informatica, 2016.

Algorithms for Kleene Algebra with Converse.
P. Brunet and D. Pous
J. of Logical and Algebraic Methods in Programming, 2016.

Enhanced Coalgebraic Bisimulation,
.pdf.
J. Rot, F. Bonchi, M. Bonsangue, D. Pous, J. Rutten, and A. Silva,
Mathematical Structures in Computer Science, 2015.

Hacking Nondeterminism with Induction and Coinduction,
.pdf.
F. Bonchi, D. Pous,
Research Highlights in Communications of the ACM, 2015.

Untyping Typed Algebras and Colouring Cyclic Linear Logic,
implementation and Coq proofs,
.pdf.
D. Pous, Logical Methods in Computer Science, 2012.

Innocent Strategies as Presheaves and Interactive Equivalences for CCS,
.pdf.
T. Hirschowitz and D. Pous,
Scientific Annals of Computer Science, 2012.

Deciding Kleene Algebras in Coq,
.pdf.
T. Braibant and D. Pous,
Logical Methods in Computer Science, 2012.

Using Bisimulation Proof Techniques for the Analysis of Distributed Abstract Machines,
.pdf.
D. Pous, Theoretical Computer Science, 2008.

A Distribution Law for CCS and a New Congruence Result for the picalculus,
.pdf.
D. Hirschkoff and D. Pous,
Logical Methods in Computer Science, 2008.

New Upto Techniques for Weak Bisimulation,
.pdf.
D. Pous,
Theoretical Computer Science, 2007.

An Efficient Abstract Machine for Safe Ambients.
D. Hirschkoff, D. Pous, and D. Sangiorgi,
Journal of Logic and Algebraic Programming, 2007.
For conferences

Companions, Codensity, and Causality,
.pdf.
D. Pous, J. Rot, to appear in Proc. FoSSaCS'17.

Coinduction all the way up,
Coq proofs,
.pdf.
D. Pous, in Proc LICS'16.

A Formal Exploration of Nominal Kleene Algebra,
.pdf,
Coq proofs.
P. Brunet, D. Pous, in Proc. MFCS'16.

Cardinalities of Finite Relations in Coq,
.pdf,
P. Brunet, D. Pous, I. Stucke, in Proc. ITP'16.

Lax Bialgebras and UpTo Techniques for Weak Bisimulations,
.pdf
F. Bonchi, D. Petrisan, D. Pous, and J. Rot, in Proc CONCUR'15.

Petri automata for Kleene allegories,
.pdf,
implementation.
P. Brunet and D. Pous, in Proc. LICS'15.

Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests,
implementation,
.pdf.
D. Pous, in Proc. POPL'15.

Bisimulations upto: beyond firstorder transition systems,
.pdf.
J.M. Madiot and D. Pous and D. Sangiorgi, in Proc. CONCUR'14.

Coinduction upto in a fibrational setting,
.pdf.
F. Bonchi and D. Petrisan and D. Pous and J. Rot, in Proc. CSLLICS'14.

Kleene Algebra with Converse,
web page,
.pdf.
P. Brunet and D. Pous, in Proc. RAMiCS'14.

Brzozowski's and UpTo Algorithms for Must Testing,
.pdf.
F. Bonchi and G. Caltais, D. Pous, and A. Silva, in Proc. APLAS'13.

Coalgebraic upto techniques,
.pdf.
D. Pous, invited talk, in Proc. CALCO'13.

Kleene Algebra with Tests and Coq Tools for while Programs,
Coq library,
.pdf.
D. Pous, in Proc. ITP'13.

Robust Reconfigurations of Component Assemblies,
Coq proofs.
F. Boyer, O. Gruber, and D. Pous, in Proc. ICSE'13.

Checking NFA equivalence with bisimulations up to congruence,
implementation and Coq proofs,
.pdf.
F. Bonchi and D. Pous, in Proc. POPL'13.

Tactics for Reasoning modulo AC in Coq,
web page,
.pdf.
T. Braibant and D. Pous, in Proc. CPP'11.

Untyping Typed Algebraic Structures and Colouring Proof
Nets of Cyclic Linear Logic,
implementation and Coq proofs,
.pdf.
D. Pous, in Proc. CSL'10.

On Bisimilarity and Substitution in Presence of Replication,
.pdf.
D. Hirschkoff and D. Pous, in Proc. ICALP'10.

An Efficient Coq Tactic for Deciding Kleene Algebras,
.pdf.
T. Braibant and D. Pous, in Proc. ITP'10.

Complete Lattices and Upto Techniques,
.pdf.
D. Pous, in Proc. APLAS'07.

A Distribution Law for CCS and a New Congruence Result for the
picalculus,
.pdf.
D. Hirschkoff, D. Pous, in Proc. FOSSACS'07
(an extended
version appeared in LMCS, 2008).

On Bisimulation Proofs for the Analysis of Distributed
Abstract Machines,
.pdf.
D. Pous, in Proc. TGC'06
(an extended
version appeared in TCS, 2008).

Weak Bisimulation up to Elaboration,
.pdf.
D. Pous, in Proc. CONCUR'06.

Upto Techniques for Weak Bisimulation,
.pdf.
D. Pous, in Proc. ICALP'05
(an extended
version appeared in TCS, 2007).

ComponentOriented Programming with Sharing: Containment is not
Ownership,
.pdf.
D. Hirschkoff, T. Hirschowitz, D. Pous, A. Schmitt, and J.B.
Stefani, in Proc. GPCE'05.

A Correct Abstract Machine for Safe Ambients,
.pdf.
D. Hirschkoff, D. Pous, and D. Sangiorgi, in Proc.
COORDINATION'05
(an extended
version appeared in JLAP, 2007).
For workshops

Decidability of Identityfree Relational Kleene lattices.
P. Brunet and D. Pous, JFLA'15.

De la KAM avec un Processus d’Ordre Supérieur.
D. Pous and A. Schmitt, JFLA'14.

Formal verification in Coq of program properties involving the global state effect.
J.G. Dumas, D. Duval, B. Ekici, and D. Pous, JFLA'14.

Innocent strategies as presheaves and interactive
equivalences for CCS,
.pdf.
T. Hirschowitz and D. Pous, in Proc. ICE'11.

Untyping Typed Algebraic Structures
(new version and Coq proofs here).
D. Pous, CAMCAD Workshop, 2009.

A Tactic for Deciding Kleene Algebras
(corresponding Coq library, ATBR).
T. Braibant and D. Pous, 1st Coq Workshop,
2009.

Encapsulation and Dynamic Modularity in the picalculus,
.pdf.
D. Hirschkoff, A. Pardon, T. Hirschowitz, S. Hym, and D Pous, 1st PLACES Workshop, 2008.
HdR Thesis
PhD Thesis
Nouveau: pour connaître mon indice de Pous, demandez à Romain Demangeon.