add DOIs
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 6 Nov 2008 12:48:20 +0000 (13:48 +0100)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 6 Nov 2008 12:48:20 +0000 (13:48 +0100)
local.css
research/publications.mdwn

index 2561991..7df7740 100644 (file)
--- a/local.css
+++ b/local.css
@@ -125,3 +125,13 @@ table.identikit tr td {
   vertical-align: top;
 }
 
+.doi_logo , .doi_logo a {
+    background: #3965bd;
+    color: white !important;
+    font-size: 80%;
+    text-decoration: none;
+    font-family: times;
+    font-weight: bold;
+    padding: 0px 1px 0px 2px;
+}
+
index f8ae62f..6c18e35 100644 (file)
@@ -7,9 +7,7 @@ in reverse chronological order.
 
 # <span title="international, peer-reviewed journals">journal articles</span>
 
- 1. <a class="paper_download" href="nrhm-overlapping-conversions.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Paolo Marinelli, Fabio Vitali, Stefano Zacchiroli.
-      **Towards the unification of formats for overlapping markup**
-      . <em>
+ 1. <a class="paper_download" href="nrhm-overlapping-conversions.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1080/13614560802316145" title="Document Object Identifier">doi&gt;</a></span> Paolo Marinelli, Fabio Vitali, Stefano Zacchiroli. **Towards the unification of formats for overlapping markup**.  <em>
        To appear in <a href="http://www.tandf.co.uk/journals/titles/13614568.asp">New Review
          of Hypermedia and Multimedia</a>, <a href="http://www.tandf.co.uk/">Taylor and Francis</a>, ISSN
        1361-4568.
@@ -17,9 +15,7 @@ in reverse chronological order.
     [[toggle id=id20 text="Abstract..."]] [[toggleable id=id20 text="""
     *Abstract:* Overlapping markup refers to the issue of how to represent data structures more expressive than trees—for example direct acyclic graphs—using markup (meta-)languages which have been designed with trees in mind—for example XML. In this paper we observe that the state of the art in overlapping markup is far from being the widespread and consistent stack of standards and technologies readily available for XML and develop a roadmap for closing the gap. In particular we present in the paper the design and implementation of what we believe to be the first needed step, namely: a syntactic conversion framework among the plethora of overlapping markup serialization formats. The algorithms needed to perform the various conversions are presented in pseudo-code, they are meant to be used as blueprints for researchers and practitioners which need to write batch translation programs from one format to the other.
     """]]
- 1. <a class="paper_download" href="mcs-disambiguation-errors.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Claudio Sacerdoti Coen, Stefano Zacchiroli.
-      **Spurious Disambiguation Errors and How to Get Rid of Them**
-      . <em>
+ 1. <a class="paper_download" href="mcs-disambiguation-errors.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Claudio Sacerdoti Coen, Stefano Zacchiroli. **Spurious Disambiguation Errors and How to Get Rid of Them**.  <em>
        To appear in <a href="http://www.cc4cm.org/mcs/">Mathematics in
          Computer Science</a>, <a href="http://www.cs.bham.ac.uk/~mmk/events/mcs/">Special Issue on
          Management of Mathematical Knowledge</a>, Springer Birkhäuser, <a href="http://www.springer.com/birkhauser/mathematics/journal/11786">ISSN
@@ -28,9 +24,7 @@ in reverse chronological order.
     [[toggle id=id19 text="Abstract..."]] [[toggleable id=id19 text="""
     *Abstract:* The disambiguation approach to the input of formulae enables users of mathematical assistants to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae however, far too many typing errors are generated; among them we want to present only errors related to the formula interpretation meant by the user, hiding errors related to other interpretations. We study disambiguation errors and how to classify them into the spurious and genuine error classes. To this end we give a general presentation of the classes of disambiguation algorithms and efficient disambiguation algorithms. We also quantitatively assess the quality of the presented error classification criteria benchmarking them in the setting of a formal development of constructive algebra.
     """]]
- 1. <a class="paper_download" href="matita.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli.
-      **User Interaction with the Matita Proof Assistant**
-      . <em>
+ 1. <a class="paper_download" href="matita.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/s10817-007-9070-5" title="Document Object Identifier">doi&gt;</a></span> Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. **User Interaction with the Matita Proof Assistant**.  <em>
        In <a href="http://www-unix.mcs.anl.gov/JAR/">Journal of Automated
          Reasoning</a>, <a href="http://springerlink.metapress.com/content/h81468706x24/">Volume
          39, Number 2, Special Issue on User Interfaces for Theorem
@@ -43,9 +37,7 @@ in reverse chronological order.
 
 # book chapters
 
- 1. <a class="paper_download" href="web30-semantics-templating.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Angelo Di Iorio, Fabio Vitali, Stefano Zacchiroli.
-      **Web Semantics via Wiki Templating**
-      . <em>
+ 1. <a class="paper_download" href="web30-semantics-templating.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Angelo Di Iorio, Fabio Vitali, Stefano Zacchiroli. **Web Semantics via Wiki Templating**.  <em>
        To appear in Handbook of research on Web 2.0, 3.0 and x.0:
        technologies, business and social applications.
       </em>
@@ -55,9 +47,7 @@ in reverse chronological order.
 
 # <span title="international, peer-reviewed conferences">conference proceedings</span>
 
- 1. <a class="paper_download" href="sac09-manners.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Angelo Di Iorio, Davide Rossi, Fabio Vitali, Stefano Zacchiroli.
-      **Where are your Manners? Sharing Best Community Practices in the Web 2.0**
-      . <em>To appear in proceedings
+ 1. <a class="paper_download" href="sac09-manners.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Angelo Di Iorio, Davide Rossi, Fabio Vitali, Stefano Zacchiroli. **Where are your Manners? Sharing Best Community Practices in the Web 2.0**.  <em>To appear in proceedings
         of <a href="http://www.acm.org/conferences/sac/sac2009/">ACM
         SAC 2009</a> (the 24th Annual ACM Symposium on Applied
         Computing), <a href="http://www.cs.unibo.it/sacwt09/">Track on
@@ -65,18 +55,14 @@ in reverse chronological order.
     [[toggle id=id23 text="Abstract..."]] [[toggleable id=id23 text="""
     *Abstract:* The Web 2.0 fosters the creation of communities by offering users a wide array of social software tools. But, while the success of these tools is based on their ability to support different interaction patterns among users by imposing as less limitations as possible, the communities they support are not free of rules (just think about the posting rules in a community forum or the editing rules in a thematic wiki). In this paper we propose a framework for the sharing of best community practices in the form of a (potentially rule-based) annotation layer that can be integrated with existing Web 2.0 community tools (with specific focus on wikis). This solution is characterized by minimal intrusiveness and plays nicely within the open spirit of the Web 2.0 by proving users with behavioral hints rather than by enforcing the strict adherence to a set of rules.
     """]]
- 1. <a class="paper_download" href="hotswup-package-upgrade.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Roberto Di Cosmo, Paulo Trezentos, Stefano Zacchiroli.
-      **Package Upgrades in FOSS Distributions: Details and Challenges**
-      . <em>In proceedings
+ 1. <a class="paper_download" href="hotswup-package-upgrade.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Roberto Di Cosmo, Paulo Trezentos, Stefano Zacchiroli. **Package Upgrades in FOSS Distributions: Details and Challenges**.  <em>In proceedings
          of <a href="http://www.hotswup.org/">HotSWUp'08 (Hot Topics
          in Software Upgrades)</a>. October 20, 2008, Nashville,
          Tennessee, USA. ACM ISBN 978-1-60558-304-4/08/10.</em>
     [[toggle id=id22 text="Abstract..."]] [[toggleable id=id22 text="""
     *Abstract:* The upgrade problems faced by Free and Open Source Software distributions have characteristics not easily found elsewhere. We describe the structure of packages and their role in the upgrade process. We show that state of the art package managers have shortcomings inhibiting their ability to cope with frequent upgrade failures. We survey current countermeasures to such failures, argue that they are not satisfactory, and sketch alternative solutions.
     """]]
- 1. <a class="paper_download" href="wiki-templating.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Angelo Di Iorio, Fabio Vitali, Stefano Zacchiroli.
-      **Wiki Content Templating**
-      . <em>
+ 1. <a class="paper_download" href="wiki-templating.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1145/1367497.1367581" title="Document Object Identifier">doi&gt;</a></span> Angelo Di Iorio, Fabio Vitali, Stefano Zacchiroli. **Wiki Content Templating**.  <em>
        In Proceedings of <a href="http://www2008.org">WWW 2008</a>: 17th
        International World Wide Web Conference. April 21-25, 2008 Beijing,
         China. ACM 978-1-60558-085-2/08/04,
@@ -86,9 +72,7 @@ in reverse chronological order.
     [[toggle id=id18 text="Abstract..."]] [[toggleable id=id18 text="""
     *Abstract:* Wiki content templating enables reuse of content structures among wiki pages. In this paper we present a thorough study of this widespread feature, showing how its two state of the art models (functional and creational templating) are sub-optimal. We then propose a third, better, model called lightly constrained (LC) templating and show its implementation in the Moin wiki engine. We also show how LC templating implementations are the appropriate technologies to push forward semantically rich web pages on the lines of (lowercase) semantic web and microformats.
     """]]
- 1. <a class="paper_download" href="steve-latvia.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Paolo Marinelli, Fabio Vitali, Stefano Zacchiroli.
-      **Streaming Validation of Schemata: the Lazy Typing Discipline**
-      . <em>
+ 1. <a class="paper_download" href="steve-latvia.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Paolo Marinelli, Fabio Vitali, Stefano Zacchiroli. **Streaming Validation of Schemata: the Lazy Typing Discipline**.  <em>
        In Proceedings of <a href="http://www.extrememarkup.com/extreme/index.html">Extreme Markup
          Languages 2007</a>: The Markup Theory and Practice Conference.
        August 7-10, 2007 Montreal, Canada.
@@ -96,9 +80,7 @@ in reverse chronological order.
     [[toggle id=id15 text="Abstract..."]] [[toggleable id=id15 text="""
     *Abstract:* Assertions, identity constraints, and conditional type assignments are (planned) features of XML Schema which rely on XPath evaluation to various ends. The allowed XPath subset exploitable in those features is trimmed down for streamability concerns partly understandable (the apparent wish to avoid buffering to determine the evaluation of an expression) and partly artificial. In this paper we dissect the XPath language in subsets with varying streamability characteristics. We also identify the larger subset which is compatible with the typing discipline we believe underlies some of the choices currently present in the XML Schema specifications. We describe such a discipline as imposing that the type of an element has to be decided when its start tag is encountered and its validity has to be when its end tag is. We also propose an alternative lazy typing discipline where both type assignment and validity assessment are fired as soon as they are available in a best effort manner. We believe our discipline is more flexible and delegate to schema authors the choice of where to place in the trade-off between using larger XPath subsets and increasing buffering requirements or expeditiousness of typing information availability.
     """]]
- 1. <a class="paper_download" href="disambiguation-errors.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Claudio Sacerdoti Coen, Stefano Zacchiroli.
-      **Spurious Disambiguation Error Detection**
-      . <em>
+ 1. <a class="paper_download" href="disambiguation-errors.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Claudio Sacerdoti Coen, Stefano Zacchiroli. **Spurious Disambiguation Error Detection**.  <em>
        In Proceedings of <a href="http://www.cs.bham.ac.uk/~mmk/events/MKM07/">MKM 2007</a>: The
        6th International Conference on Mathematical Knowledge Management.
        Hagenberg, Austria -- 27-30 June 2007. <a href="http://www.springerlink.com/content/u10172854312/">LNAI
@@ -108,9 +90,7 @@ in reverse chronological order.
     [[toggle id=id14 text="Abstract..."]] [[toggleable id=id14 text="""
     *Abstract:* The disambiguation approach to the input of formulae enables the user to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae we want to present only errors related to the interpretation meant by the user, hiding errors related to other interpretations (spurious errors). We propose a heuristic to recognize spurious errors, which has been integrated with the disambiguation algorithm of [1].
     """]]
- 1. <a class="paper_download" href="streaming-co-constraints.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Paolo Marinelli, Stefano Zacchiroli.
-      **Co-Constraint Validation in a Streaming Context**
-      . <em>
+ 1. <a class="paper_download" href="streaming-co-constraints.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Paolo Marinelli, Stefano Zacchiroli. **Co-Constraint Validation in a Streaming Context**.  <em>
        In Proceedings of <a href="http://2006.xmlconference.org/">XML 2006</a>,
        "The world's oldest and biggest XML conference".  <em>Award</em>: Winner
        of the <a href="http://2006.xmlconference.org/scholarship.html">XML
@@ -120,9 +100,7 @@ in reverse chronological order.
     [[toggle id=id13 text="Abstract..."]] [[toggleable id=id13 text="""
     *Abstract:* In many use cases applications are bound to be run consuming only a limited amount of memory. When they need to validate large XML documents, they have to adopt streaming validation, which does not rely on an in-memory representation of the whole input document. In order to validate an XML document, different kinds of constraints need to be verified. Co-constraints---which relate the content of elements to the presence and values of other attributes or elements---are one such kind of constraints. In this paper we propose an approach to the problem of validating in a streaming fashion an XML document against a schema also specifying co-constraints. We describe how the streaming evaluation of co-constraints influences the output of the validation process. Our proposal makes use of the validation language SchemaPath, a light extension to XML Schema, adding conditional type assignment for the support of co-constraints. The paper is based on the description of our streaming SchemaPath validator.
     """]]
- 1. <a class="paper_download" href="matita-crafting.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli.
-      **Crafting a Proof Assistant**
-      . <em>
+ 1. <a class="paper_download" href="matita-crafting.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. **Crafting a Proof Assistant**.  <em>
        In Proceedings of <a href="http://www.cs.nott.ac.uk/types06/">Types
          2006</a>: Types for Proofs and Programs. Nottingham, UK -- April
        18-21, 2006.  <a href="http://www.springerlink.com/content/u4h217614314/">LNCS
@@ -132,9 +110,7 @@ in reverse chronological order.
     [[toggle id=id10 text="Abstract..."]] [[toggleable id=id10 text="""
     *Abstract:* Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based---as Coq---on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.
     """]]
- 1. <a class="paper_download" href="tinycals.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli.
-      **Tinycals: Step by Step Tacticals**
-      . <em>
+ 1. <a class="paper_download" href="tinycals.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.entcs.2006.09.026" title="Document Object Identifier">doi&gt;</a></span> Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. **Tinycals: Step by Step Tacticals**.  <em>
        In Proceedings of
        <a href="http://www.ags.uni-sb.de/~omega/workshops/UITP06/">UITP
          2006</a>: User Interfaces for Theorem Provers. Seattle, WA -- August
@@ -143,9 +119,7 @@ in reverse chronological order.
     [[toggle id=id8 text="Abstract..."]] [[toggleable id=id8 text="""
     *Abstract:* Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this paper we discuss how these ingredients do not interact well with user interfaces based on the same interaction paradigm of Proof General (the de facto standard in this field), identifying in the coarse-grainedness of tactical evaluation the key problem. We propose Tinycals as an alternative to a subset of LCF tacticals, showing that the user does not experience the same problem if tacticals are evaluated in a more fine-grained manner. We present the formal operational semantics of tinycals as well as their implementation in the Matita proof assistant.
     """]]
- 1. <a class="paper_download" href="constrainedwiki.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Angelo Di Iorio, Stefano Zacchiroli.
-      **Constrained Wiki: an Oxymoron?**
-      . <em>
+ 1. <a class="paper_download" href="constrainedwiki.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1145/1149453.1149471" title="Document Object Identifier">doi&gt;</a></span> Angelo Di Iorio, Stefano Zacchiroli. **Constrained Wiki: an Oxymoron?**.  <em>
        In Proceedings of
        <a href="http://www.wikisym.org/ws2006/">WikiSym 2006</a>: the 2006
        International Symposium on Wikis. Odense, Denmark -- August 21-23, 2006.
@@ -156,9 +130,7 @@ in reverse chronological order.
     [[toggle id=id7 text="Abstract..."]] [[toggleable id=id7 text="""
     *Abstract:* In this paper we propose a new wiki concept -- light constraints -- designed to encode community best practices and domain-specific requirements, and to assist in their application. While the idea of constraining user editing of wiki content seems to inherently contradict "The Wiki Way", it is well-known that communities of users involved in wiki sites have the habit of establishing best authoring practices. For domain-specific wiki systems which process wiki content, it is often useful to enforce some well-formedness conditions on specific page contents. This paper describes a general framework to think about the interaction of wiki system with constraints, and presents a generic architecture which can be easily incorporated into existing wiki systems to exploit the capabilities enabled by light constraints.
     """]]
- 1. <a class="paper_download" href="notation.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Luca Padovani, Stefano Zacchiroli.
-      **From Notation to Semantics: There and Back Again**
-      . <em>
+ 1. <a class="paper_download" href="notation.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Luca Padovani, Stefano Zacchiroli. **From Notation to Semantics: There and Back Again**.  <em>
        In Proceedings of <a href="http://www.mkm-ig.org/meetings/mkm06/">MKM
          2006</a>: The 5th International Conference on Mathematical Knowledge
        Management.  Wokingham, UK -- August 11-12, 2006. <a href="http://www.springerlink.com/content/978-3-540-37104-5/">LNAI
@@ -168,9 +140,7 @@ in reverse chronological order.
     [[toggle id=id6 text="Abstract..."]] [[toggleable id=id6 text="""
     *Abstract:* Mathematical notation is a structured, open, and ambiguous language. In order to support mathematical notation in MKM applications one must necessarily take into account presentational as well as semantic aspects. The former are required to create a familiar, comfortable, and usable interface to interact with. The latter are necessary in order to process the information meaningfully. In this paper we investigate a framework for dealing with mathematical notation in a meaningful, extensible way, and we show an effective instantiation of its architecture to the field of interactive theorem proving. The framework builds upon well-known concepts and widely-used technologies and it can be easily adopted by other MKM applications.
     """]]
- 1. <a class="paper_download" href="whelp.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli.
-      **A Content Based Mathematical Search Engine: Whelp**
-      . <em>
+ 1. <a class="paper_download" href="whelp.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. **A Content Based Mathematical Search Engine: Whelp**.  <em>
        In Proceedings of
        <a href="http://types2004.lri.fr/">TYPES 2004</a> conference: Types for
        Proofs and Programs. Paris, France -- December 15-18, 2004.
@@ -181,9 +151,7 @@ in reverse chronological order.
     [[toggle id=id5 text="Abstract..."]] [[toggleable id=id5 text="""
     *Abstract:* The prototype of a content based search engine for mathematical knowledge supporting a small set of queries requiring matching and/or typing operations is described. The prototype, called Whelp, exploits a metadata approach for indexing the information that looks far more flexible than traditional indexing techniques for structured expressions like substitution, discrimination, or context trees. The prototype has been instantiated to the standard library of the Coq proof assistant extended with many user contributions.
     """]]
- 1. <a class="paper_download" href="gmetadom.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Luca Padovani, Claudio Sacerdoti Coen, Stefano Zacchiroli.
-      **A Generative Approach to the Implementation of Language Bindings for the Document Object Model**
-      . <em>
+ 1. <a class="paper_download" href="gmetadom.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Luca Padovani, Claudio Sacerdoti Coen, Stefano Zacchiroli. **A Generative Approach to the Implementation of Language Bindings for the Document Object Model**.  <em>
        In Proceedings of <a href="http://www.gpce.org/04/">GPCE'04</a> Third
        International Conference on Generative Programming and Component
        Engineering. Vancouver, Canada -- October 24-28, 2004
@@ -195,9 +163,7 @@ in reverse chronological order.
     [[toggle id=id4 text="Abstract..."]] [[toggleable id=id4 text="""
     *Abstract:* The availability of a C implementation for the Document Object Model (DOM) gives the interesting opportunity of generating bindings for different programming languages automatically. Because of the DOM bias towards Java-like languages, a C implementation that fakes objects, inheritance, polymorphism, exceptions and uses reference-counting introduces a gap between the API specification and its actual implementation that the bindings should try to close. In this paper we overview the generative approach in this particular context and apply it for the generation of C++ and OCaml bindings.
     """]]
- 1. <a class="paper_download" href="mathsearch.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Andrea Asperti, Stefano Zacchiroli.
-      **Searching Mathematics on the Web: State of the Art and Future Developments**
-      . <em>
+ 1. <a class="paper_download" href="mathsearch.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Andrea Asperti, Stefano Zacchiroli. **Searching Mathematics on the Web: State of the Art and Future Developments**.  <em>
        In Proceedings of
        <a href="http://eic-ecm4.sub.uni-goettingen.de/">New Developments in
          Electronic Publishing of Mathematics 2004</a>.
@@ -206,9 +172,7 @@ in reverse chronological order.
     [[toggle id=id3 text="Abstract..."]] [[toggleable id=id3 text="""
     *Abstract:* A huge amount of mathematical knowledge is nowadays available on the World Wide Web. Many different solutions and technologies for searching that knowledge have been developed as well. We present the state of the art of searching mathematics on the Web, giving some insight on future developments in this area.
     """]]
- 1. <a class="paper_download" href="disambiguation.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Claudio Sacerdoti Coen, Stefano Zacchiroli.
-      **Efficient Ambiguous Parsing of Mathematical Formulae**
-      . <em>
+ 1. <a class="paper_download" href="disambiguation.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Claudio Sacerdoti Coen, Stefano Zacchiroli. **Efficient Ambiguous Parsing of Mathematical Formulae**.  <em>
        In Proceedings of <a href="http://www.mkm-ig.org/meetings/mkm04/">MKM
          2004</a> Third International Conference on Mathematical Knowledge
        Management. September 19-21, 2004 Bialowieza - Poland.
@@ -220,9 +184,7 @@ in reverse chronological order.
     [[toggle id=id2 text="Abstract..."]] [[toggleable id=id2 text="""
     *Abstract:* Mathematical notation has the characteristic of being ambiguous: operators can be overloaded and information that can be deduced is often omitted. Mathematicians are used to this ambiguity and can easily disambiguate a formula making use of the context and of their ability to find the right interpretation. Software applications that have to deal with formulae usually avoid these issues by fixing an unambiguous input notation. This solution is annoying for mathematicians because of the resulting tricky syntaxes and becomes a show stopper to the simultaneous adoption of tools characterized by different input languages. In this paper we present an efficient algorithm suitable for ambiguous parsing of mathematical formulae. The only requirement of the algorithm is the existence of a validity predicate over abstract syntax trees of incomplete formulae with placeholders. This requirement can be easily fulfilled in the applicative area of interactive proof assistants, and in several other areas of Mathematical Knowledge Management.
     """]]
- 1. <a class="paper_download" href="hbugs.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Claudio Sacerdoti Coen, Stefano Zacchiroli.
-      **Brokers and Web-Services for Automatic Deduction: a Case Study**
-      . <em>
+ 1. <a class="paper_download" href="hbugs.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Claudio Sacerdoti Coen, Stefano Zacchiroli. **Brokers and Web-Services for Automatic Deduction: a Case Study**.  <em>
        In Proceedings of
        <a href="http://www-calfor.lip6.fr/~rr/Calculemus03/">Calculemus
          2003</a>
@@ -236,9 +198,7 @@ in reverse chronological order.
 
 # <span title="official research reports of research institutions">technical reports</span>
 
- 1. <a class="paper_download" href="mancoosi-d5.1.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Ralf Treinen, Stefano Zacchiroli.
-      **Description of the CUDF Format**
-      . <em>
+ 1. <a class="paper_download" href="mancoosi-d5.1.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Ralf Treinen, Stefano Zacchiroli. **Description of the CUDF Format**.  <em>
        <a href="http://www.mancoosi.org">Mancoosi project</a>
        deliverable,
        <a href="http://www.mancoosi.org/deliverables/d5.1.pdf">D5.1</a>,
@@ -247,18 +207,14 @@ in reverse chronological order.
     [[toggle id=id24 text="Abstract..."]] [[toggleable id=id24 text="""
     *Abstract:* This document contains several related specifications, taken together they describe the document formats related to the solver competition which will be organized by Mancoosi. In particular, this document describes: DUDF (Distribution Upgradeability Description Format), the document format to be used to submit upgrade problem instances from user machines to a (distribution-specific) database of upgrade problems; CUDF (Common Upgradeability Description Format), the document format used to encode upgrade problems, abstracting over distribution-specific details. Solvers taking part in the competition will be fed with input in CUDF format.
     """]]
- 1. <a class="paper_download" href="flea.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Luca Padovani, Stefano Zacchiroli.
-      **Stream Processing of XML Documents Made Easy with LALR(1) Parser Generators**
-      . <em>
+ 1. <a class="paper_download" href="flea.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Luca Padovani, Stefano Zacchiroli. **Stream Processing of XML Documents Made Easy with LALR(1) Parser Generators**.  <em>
        <a href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2007.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2007-23">Technical
          report UBLCS-2007-23</a>, September 2007, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a>.
       </em>
     [[toggle id=id17 text="Abstract..."]] [[toggleable id=id17 text="""
     *Abstract:* Because of their fully annotated structure, XML documents are normally believed to require a straightforward parsing phase. However, the standard APIs for accessing their content (the Document Object Model and the Simple API for XML) provide a programming interface that is very low-level and is thus inadequate for the recognition of any structure that is not isomorphic to its XML encoding. Even when the document undergoes validation, its unmarshalling into application-specific data using these APIs requires poorly maintainable, tedious-to-write, and possibly inefficient code. We describe a technique for the simultaneous parsing, validation, and unmarshalling of XML documents that combines a stream-oriented XML parser with a LALR(1) parser in order to guarantee efficient stream processing, expressive validation capabilities, and the possibility to associate user-provided actions with specific patterns occurring in the source documents.
     """]]
- 1. <a class="paper_download" href="wiki-templating-tr.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Angelo Di Iorio, Fabio Vitali, Stefano Zacchiroli.
-      **Templating Wiki Content for Fun and Profit**
-      . <em>
+ 1. <a class="paper_download" href="wiki-templating-tr.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Angelo Di Iorio, Fabio Vitali, Stefano Zacchiroli. **Templating Wiki Content for Fun and Profit**.  <em>
        <a href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2007.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2007-21">Technical
          report UBLCS-2007-21</a>, August 2007, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a>.
       </em>
@@ -268,9 +224,7 @@ in reverse chronological order.
 
 # dissertations
 
- 1. <a class="paper_download" href="phd-thesis.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Stefano Zacchiroli.
-      **User Interaction Widgets for Interactive Theorem Proving**
-      . <em>
+ 1. <a class="paper_download" href="phd-thesis.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Stefano Zacchiroli. **User Interaction Widgets for Interactive Theorem Proving**.  <em>
        Ph.D. dissertation, <a href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2007.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2007-10">Technical
          report UBLCS-2007-10</a>, March 2007, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a> (advisor: <a href="http://www.cs.unibo.it/~asperti">Andrea Asperti</a>; refereed
        by: <a href="http://www.ags.uni-sb.de/~chris/">Christoph
@@ -280,18 +234,14 @@ in reverse chronological order.
     [[toggle id=id12 text="Abstract..."]] [[toggleable id=id12 text="""
     *Abstract:* Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant---Coq---with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or "undo") past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathML-Presentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.
     """]]
- 1. <a class="paper_download" href="master-thesis.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Stefano Zacchiroli.
-      **Web services per il supporto alla dimostrazione interattiva (Web services for interactive theorem proving)**
-      . <em>
+ 1. <a class="paper_download" href="master-thesis.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Stefano Zacchiroli. **Web services per il supporto alla dimostrazione interattiva (Web services for interactive theorem proving)**.  <em>
        Master thesis (Italian only), March 2003, <a href="http://www.cs.unibo.it">Department of Computer Science</a>, <a href="http://www.unibo.it">University of Bologna</a> (advisor: <a href="http://www.cs.unibo.it/~asperti">Andrea Asperti</a>; refereed
        by: <a href="http://www.cs.unibo.it/~busi">Nadia Busi</a>).
       </em>
 
 # miscellanea
 
- 1. <a class="paper_download" href="debconf8-mancoosi.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Ralf Treinen, Stefano Zacchiroli.
-      **Solving package dependencies: from EDOS to Mancoosi**
-      . <em>In proceedings
+ 1. <a class="paper_download" href="debconf8-mancoosi.pdf"><img src="../../img/pdf-format-logo.png" alt=""/>[.pdf]</a> Ralf Treinen, Stefano Zacchiroli. **Solving package dependencies: from EDOS to Mancoosi**.  <em>In proceedings
        of <a href="http://debconf8.debconf.org/">DebConf8</a> (9th
        annual conference of
        the <a href="http://www.debian.org">Debian</a> project