Damien Pous

Researcher at the CNRS, member of the Plume team, external collaborator of the Sardes project.

Personal Data

Research

I supervised the PhD of Thomas Braibant: we developped Coq tools that should make it possible, at some point, to study and certify distributed systems (see our PiCoq project). We released a reflexive tactic for deciding Kleene algebras; the current state of the corresponding library (ATBR) can be found there. we pursued this work by implementing tools for rewriting modulo AC

I just released the Coq RelationAlgebra library, which provides a modular hierarchy for various fragments of Relation algebra, and includes a tactic for deciding Kleene algebras with Tests (KAT).

I also played with linear logic, thanks to the CHoCo band members, and more recently with finite automata, together with Filippo Bonchi.

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

I did my PhD under the supervision of Daniel Hirschkoff. Here is my dissertation (in french). It is about 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

• Untyping Typed Algebras and Colouring Cyclic Linear Logic, .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 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

• Checking NFA equivalence with bisimulations up to congruence, web page, .pdf.
  F. Bonchi and D. Pous, to appear in Proc. POPL'13.
  
• Robust Reconfigurations of Component Assemblies, web page.
  F. Boyer, O. Gruber, and D. Pous, to appear in Proc. ICSE'13.
  
• 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)

• 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

• A new algorithm for NFA language equivalence (joint work with Filippo Bonchi).
• Optimised proof search algorithm for cyclic linear logic.

Abstract Machines (OCaml)

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

Teaching

• Concurrency theory and Implicit Complexity (with Patrick Baillot, M2 ENS Lyon, 2012-2013)
• Floating point arithmetic and formal proofs (with Jean-Michel Muller and Laurent Théry, 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).

Personal Page