Damien Pous

Personal Data

eMail : Damien dot Pous at inria dot fr
Office : (+33) 4 76 61 52 95 B111, INRIA Rhône-Alpes, 655, avenue de l'Europe, Montbonnot 38334 Saint Ismier		Home : (+33)9 53 27 49 82 8 rue René Thomas 38000 Grenoble

Situation

Researcher at the CNRS, in the SARDES project (LIG/INRIA). I am supervising the PhD of Thomas Braibant: we develop Coq tools that should make it possible, at some point, to study and certify distributed systems. We released a reflexive tactic for deciding Kleene algebras; the current state of the corresponding library (ATBR) can be found there. we pursue this work by implementing other tools (rewriting modulo AC, other decision procedures).

I also recently played with linear logic, thanks to the CHoCo band members.

I did a post-doc at UPenn, with Benjamin C. Pierce and Aaron Bohannon.

I did my PhD under the supervision of Daniel Hirschkoff, in the Plume team. Here is my dissertation (in french). It deals with up-to techniques for bisimulations in the context of distributed and mobile langages (CCS, pi, kells, join...),

Publications (dblp, .bib)

Book chapter

Enhancements of the coinductive proof method.
D. Pous and D. Sangiorgi, in Advanced Topics in Bisimulation and Coinduction, D. Sangiorgi and J. Rutten, editors. Cambridge University Press, 2011.

In journals

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 pi-calculus, .pdf.
D. Hirschkoff and D. Pous, Logical Methods in Computer Science, 2008.
New Up-to Techniques for Weak Bisimulation.
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

Tactics for Reasoning modulo AC in Coq, web page.
T. Braibant and D.Pous, in Proc. CPP'11, LNCS 7086, December 2011.
Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic, web page, .pdf.
D. Pous, in Proc. CSL'10, LNCS 6247, August 2010.
On Bisimilarity and Substitution in Presence of Replication, .pdf.
D. Hirschkoff and D. Pous, in Proc. ICALP'10, LNCS 6199, July 2010.
An Efficient Coq Tactic for Deciding Kleene Algebras, .pdf.
T. Braibant and D. Pous, in Proc. ITP'10, LNCS 6172, July 2010.
Complete Lattices and Up-to Techniques, .pdf.
D. Pous, in Proc. APLAS'07, LNCS 4807, November 2007.
A Distribution Law for CCS and a New Congruence Result for the pi-calculus, .pdf.
D. Hirschkoff, D. Pous, in Proc. FOSSACS'07, LNCS 4423, April 2007 (an extended version appeared in LMCS, 2008).
On Bisimulation Proofs for the Analysis of Distributed Abstract Machines, .pdf.
D. Pous, in Proc. TGC'06, LNCS 4661, November 2006 (an extended version appeared in TCS, 2008)
Weak Bisimulation up to Elaboration, .pdf.
D. Pous, in Proc. CONCUR'06, LNCS 4137, August 2006.
Up-to Techniques for Weak Bisimulation, .pdf.
D. Pous, in Proc. ICALP'05, LNCS 3580, July 2005 (an extended version appeared in TCS, 2007).
Component-Oriented Programming with Sharing: Containment is not Ownership, .pdf.
D. Hirschkoff, T. Hirschowitz, D. Pous, A. Schmitt, and J.B. Stefani, in Proc. 4th GPCE, LNCS 3676, September 2005.
A Correct Abstract Machine for Safe Ambients, .pdf.
D. Hirschkoff, D. Pous, and D. Sangiorgi, in Proc. COORD'05, LNCS 3454, April 2005 (an extended version appeared in JLAP, 2007)

For workshops

Innocent strategies as presheaves and interactive equivalences for CCS.
T. Hirschowitz and D. Pous, in Proc. ICE'11, EPTCS 59, June 2011.
Untyping Typed Algebraic Structures (new version and Coq proofs here).
D. Pous, CAM-CAD Workshop, October 2009.
A Tactic for Deciding Kleene Algebras (corresponding Coq library, ATBR).
T. Braibant and D. Pous, 1st Coq Workshop, August 2009.
Encapsulation and Dynamic Modularity in the pi-calculus
D. Hirschkoff, A. Pardon, T. Hirschowitz, S. Hym, and D Pous, 1st PLACES Workshop, June, 2008.

PhD Thesis

Techniques modulo pour les bisimulations (in french), ENS Lyon, February, 2008.

Computer related stuff

Formal proofs (COQ)

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.

Distributed Abstract Machines (OCaml)

Teaching

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).

Personal Page

Antoine Venaille