logo for the research page
[homepage.git] / research.mdwn
1 [[img img/applications-science.png link="no" class="flow" alt="science"]]
2 My main job is doing research (and [[teaching]]) at the [Department of Computer
3 Science](http://www.cs.unibo.it) of the [University of
4 Bologna](http://www.unibo.it). My current and not-so current research interests
5 are summarized below, a list of my **[[publications]]** on available in a
6 [[separate_page|publications]].
7
8 # research interests
9
10  * type theory and in particular **proof assistants** / interactive theorem
11  provers. I've been one of the architect of the [Matita proof
12  assistant](http://matita.cs.unibo.it), though now I'm contributing code more
13  sparingly; both my master and Ph.D. [[theses|publications]] have been about
14  Matita. I've also worked on distributed digital libraries of formalized
15  mathematics, such as the [HELM](http://helm.cs.unibo.it) library
16
17  * **web technologies**, in particular: type systems for typing XML trees (I'm
18  currently a member of [W3C](http://www.w3.org)'s [XML Schema working
19  group](http://www.w3.org/XML/Schema)) and document validation, overlapping
20  markup, web collaboration (as in [[wikipedia wiki]]s) and its interaction with
21  content constraints
22
23  * **free software**, in particular software engineering applications to wide
24  software repositories (the typical use case of GNU/Linux distributions) and the
25  application of formal methods to them to various ends (for example for
26  dependency handling)