Damien Pous

Coordonnées

Situation

Chercheur en lutte au CNRS, dans le projet SARDES (LIG). Je travaille actuellement avec Thomas Braibant au développement d'outils Coq qui permettront, à long terme, d'étudier et certifier des systèmes distribués. Nous venons de terminer une tactique réflexive permettant de décider les algèbres de Kleene; nous comptons continuer dans cette direction, en implémentant d'autres procédures de décisions. L'état courant de la librairie Coq correspondante (ATBR) se trouve ici.

Avant j'ai travaillé dans l'équipe plumitive du laboratoire d'informatique de l'École Normale Supérieure de Lyon, sous la direction de Daniel Hirschkoff, j'y ai effectué une thèse sur les techniques de preuve pour la bisimulation (techniques modulo) et plus généralement sur la théorie des langages distribués et mobiles (pi, kells, join...),

Questions ouvertes

• En quoi le découpage du CNRS en instituts favorise-t'il l'interdisciplinarité ?
• Le CNRS, fort des grands succès passés et présents, n'a t'il pas les moyens d'influencer le gouvernement ?
• Face à la diminution du nombre de postes de chercheurs, à la dégradation des conditions de travail des enseignants-chercheurs, à la précarisation du statut des doctorants, combien de jeunes auront envie de se lancer dans la recherche demain ?
• Comment la recherche peut-elle être indépendante et objective lorsqu'elle est financée sur projet ?
• Combien de temps dois-je consacrer à la rédaction de rapports, à la relecture de rapports, à la recherche de budgets ?
• Comment est évaluée la recherche découlant du crédit impôt recherche ?
• 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 ?

Publications (dblp, .bib)

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

• 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 (extended version to appear in LMCS).
  
• On Bisimulation Proofs for the Analysis of Distributed Abstract Machines, .pdf.
  D. Pous, in Proc. TGC'06, LNCS 4661, November 2006
  
• Weak Bisimulation up to Elaboration, .pdf.
  D. Pous, in Proc. CONCUR 2006, LNCS 4137, Springer Verlag, Bonn, Germany, 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

Pour des workchops

• Untyping Typed Algebraic Structures, .pdf.
  D. Pous, CAM-CAD Workshop, October 2009.
  
• A Tactic for Deciding Kleene Algebras, .pdf.
  T. Braibant and D. Pous, in Proc. 1st Coq Workshop, August 2009.
  

Thèse

• Techniques modulo pour les bisimulations: .pdf.

Travaux à base d'ordinateur

Preuves assistées (COQ)

• Algebraic Tools for Binary Relations (dont une tactique pour decider les algèbres de Kleene).
• 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.
• Librairie pour l'exécution de processus distribués et mobiles.
• Implantation distribuée d'une machine abstraite pour une variante du Kell-calcul, incluant la primitive de passivation (non publiée pour l'instant).

Divers

• Machine graphique permettant d'interpréter de façon ludique différentes variantes du calcul des Mobile Ambients.
• Portage de l'API LIRC sous OCaml.
• Système générique de Makefile pour OCaml, avec analyse fine des dépendances.
• Synthétiseur de scènes 3D, par lançage de rayons.
• Jeu en 3D (openGL) pour apprendre la programmation aux enfants.
• Compilateur pour un sous-langage de Fortran.
• ...autres petits programmes OCaml.

Enseignements

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