science My main job is doing research (and teaching) at the Laboratoire PPS of the Université Paris Diderot - Paris 7. My current and not-so current research interests are summarized below, a list of my publications is available from a separate page.

research interests

  • free software and how formal methods can be applied to address the complexity of the scenarios brought by the open source development model. I'm currently a member of the mancoosi research project, which is addressing some of this challenges, in particular the upgrade problem of packages in GNU/Linux distributions

  • type theory and in particular proof assistants / interactive theorem provers. I've been one of the architect of the Matita proof assistant, though now I'm contributing code more sparingly; both my master and Ph.D. theses have been about Matita. I've also worked on distributed digital libraries of formalized mathematics, such as the HELM library

  • web technologies, in particular: type systems for typing XML trees (I'm currently a member of W3C's XML Schema working group) and document validation, overlapping markup, web collaboration (as in wikis) and its interaction with content constraints


A list of my publications is available on a dedicated page.


I've been involved in a number of scientific committees.