Damien Pous

Personal Data

iMail : Damien dot Pous at inria dot fr
Office : (+33) 4 76 61 52 95 B105, 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 CNRS, in the SARDES project (LIG/INRIA). I am currently working with Thomas Braibant: we develop Coq tools Coq that should make it possible, at some point, to study and certify distributed systems. We have just released a reflexive tactic for deciding Kleene algebras; we plan to pursue this work by implementing other decision procedures. The current state of the corresponding library (ATBR) can be found there.

I also recently played with linear logic

I previously worked in the Plume team, (École Normale Supérieure de Lyon, France). I did a PhD under the supervision of Daniel Hirschkoff, here is my dissertation. I studied proof techniques for bisimulation (up-to techniques), as well as programming langages for concurrency, distribution and mobility (CCS, pi, Kells, join...).

Publications (dblp, .bib)

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

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

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

Technique modulo pour les bisimulations, ENS Lyon, February, 2008.

Computer related stuff

Formal proofs (COQ)

Algebraic Tools for Binary Relations (includes a tactic for deciding Kleene algebras).
Formalisation of the entire ICALP'05 article.
Certified compiler from recursive functions to Minski machines.

Distributed Abstract Machines (OCaml)

Teaching

Bisimulations and process calculi (with Alan Schmitt, MSTII, UJF Grenoble, 2010).
Natural deduction (DLST, UJF Grenoble, 2010).
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).