Damien Pous
Researcher at the CNRS, member of the Plume team, external
collaborator of the Sardes
project.
Version française
Personal Data
eMail:
Damien dot Pous at ens-lyon dot fr
|
Office: (+33) 4 37 28 76 47
LUG-176, LIP, ENS Lyon
46 allee d'Italie 69364 Lyon
|
|
Home: (+33)9 53 27 49 82
199 rue Vendome 69003 Lyon
|
Announcements
Please attend to CaCos,
a sattelite workshop of ISSAC, dedicated to
categorical science and proof assistant developments, and what they
could bring to computer algebra. (Grenoble, the 26th of July.)
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 the 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 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
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
Computer related stuff
Formal proofs (COQ)
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).