research.mdwn

   1 [[!img img/applications-science.png link="no" class="flow" alt="science"]] My
   2 main job is doing research (and [[teaching]]) at the [Laboratoire
   3 PPS](http://www.univ-paris-diderot.fr/) of the [Université Paris Diderot - Paris
   4 7](http://www.univ-paris-diderot.fr/). My current and not-so current research
   5 interests are summarized below, a list of my **[[publications]]** is available
   6 from a [[separate page|publications]].
   7
   8 # research interests
   9
  10 * **free software** and how formal methods can be applied to address the
  11   complexity of the scenarios brought by the open source development model. I'm
  12   currently a member of the [mancoosi](http://www.mancoosi.org) research
  13   project, which is addressing some of this challenges, in particular the
  14   *upgrade problem* of packages in GNU/Linux distributions
  15
  16 * type theory and in particular **proof assistants** / interactive theorem
  17   provers. I've been one of the architect of the
  18   [Matita proof assistant](http://matita.cs.unibo.it), though now I'm
  19   contributing code more sparingly; both my master and
  20   Ph.D. [[theses|publications]] have been about Matita. I've also worked on
  21   distributed digital libraries of formalized mathematics, such as the
  22   [HELM](http://helm.cs.unibo.it) library
  23
  24 * **web technologies**, in particular: type systems for typing XML trees (I'm
  25   currently a member of [W3C](http://www.w3.org)'s
  26   [XML Schema working group](http://www.w3.org/XML/Schema)) and document
  27   validation, overlapping markup, web collaboration (as in
  28   [[!wikipedia wiki]]s) and its interaction with content constraints
  29
  30 # publications
  31
  32 A list of my publications is available on a [[dedicated page|publications]].
  33
  34 # committees
  35
  36 I've been involved in a number of [[scientific committees|committees]].