Damien Pous

Chercheur au CNRS, membre de l'équipe Plume, collaborateur externe de l'EPI Sardes.

Coordonnées

Recherche

J'ai encadré la thèse de Thomas Braibant: nous avons développé des outils Coq qui permettront, à long terme, d'étudier et certifier des systèmes distribués (cf. le projet PiCoq). Nous avons en particulier défini une tactique réflexive permettant de décider les algèbres de Kleene; l'état courant de la librairie Coq correspondante (ATBR) se trouve ici, ainsi que des outils pour la réécriture modulo AC.

Récemment, j'ai aussi joué à colorier des réseaux de preuve en logique linéaire, grâce aux membres du projet CHoCo.

J'ai fait un post-doc à l'Université de Pennsylvanie, avec Benjamin C. Pierce et Aaron Bohannon.

J'ai effectué ma thèse sous la direction de Daniel Hirschkoff dans l'équipe Plume. Ma dissertation se trouve ici, elle porte sur les techniques de preuve pour la bisimulation (techniques modulo) dans le contexte de la théorie des langages distribués et mobiles (CCS, pi, kells, join...),

Questions ouvertes

• Est-ce que l'université restera accessible à tous ? Avec l'autonomie, les universités pourront-elles fixer à leur guise les droits d'inscription, et opérer par là même une sélection sociale ?
• En quoi le découpage du CNRS en instituts favorise-t'il l'interdisciplinarité ?
• Comment la recherche peut-elle être indépendante et objective lorsqu'elle est financée sur projet ?
• Comment est évaluée la recherche découlant du crédit impôt recherche ?

Publications (dblp, .bib)

Chapitre de livre

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

Dans des revues

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

Pour des conférences

• Tactics for Reasoning modulo AC in Coq, page web.
  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, page web, .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)

Pour des workshops

• Innocent strategies as presheaves and interactive equivalences for CCS.
  T. Hirschowitz and D. Pous, in Proc. ICE'11, EPTCS 59, June 2011.
  
• Des transparents sur notre utilisation des typeclasses en Coq pour les (petites) hiérarchies algébriques et la réification.
  (31/03/2011, GT Coq on reification and generic tactics, avec le fichier pour la demo atbr.v).
• Rewriting modulo Associativity and Commutativity in Coq (page web).
  T. Braibant and D. Pous, travaux en cours qui seront présentés au second Coq Workshop, Juillet 2010.
  
• Untyping Typed Algebraic Structures (nouvelle version et preuves Coq ici).
  D. Pous, CAM-CAD Workshop, Octobre 2009.
  
• A Tactic for Deciding Kleene Algebras (librairie Coq correspondante, 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.
  

Thèse

• Techniques modulo pour les bisimulations, ENS Lyon, Février 2008.

Travaux à base d'ordinateur

Preuves assistées (COQ)

• Certification of robust reconfiguration algorithms (avec Fabienne Boyer et Olivier Gruber).
• Outils algébriques pour les relations binaires (dont une tactique pour decider les algèbres de Kleene---avec Thomas Braibant).
• Plugin pour la réécriture modulo associativité et commutativité (avec Thomas Braibant).
• Formalisation de l'article présenté à ICALP'05.
• Compilateur certifié des fonctions récursives vers les machines de Minski.

Machines abstraites distribuées (OCaml)

• Implantation distribuée d'une machine abstraite pour le calcul des Safe Ambient.
• Machine graphique permettant d'interpréter de façon ludique différentes variantes du calcul des Mobile Ambients.

Enseignements

• Premiers pas avec Coq (pour les journées nationales de l'APMEP, Grenoble, 2011)
• Coq: de la théorie à la pratique (avec Alan Schmitt, école doctorale MSTII, UJF Grenoble, 2011).
• Bisimulations et calculs de processus (avec Alan Schmitt, école doctorale MSTII, UJF Grenoble, 2010).
• Déduction naturelle (TDs de L1, DLST, UJF Grenoble, 2010, 2011).
• Monitorat à l'ENS Lyon:
  • TPs de programmation (L3, 2005-2006, 2006-2007).
  • TDs de logique, sémantique et réécriture (L3, 2005-2006, 2006-2007, 2007-2008).
  • TDs de preuves assistées (COQ) (M1-M2, 2007-2008).
• Ateliers de découverte de l'informatique pour les enfants de l'école primaire Claudius Berthelier (2004-2005).
• TDs de Maple, pour les classes préparatoires du Lycée du Parc (2002-2004).

Page perso

Nouveau: pour connaître mon indice de Pous, demandez à Romain Demangeon.