regenerate publication list
authorStefano Zacchiroli <zack@debian.org>
Thu, 20 Dec 2007 18:41:23 +0000 (19:41 +0100)
committerStefano Zacchiroli <zack@debian.org>
Thu, 20 Dec 2007 18:41:23 +0000 (19:41 +0100)
research/publications.mdwn

index 3d359e4..6612bc8 100644 (file)
@@ -5,7 +5,7 @@
          Reasoning</a>, <a href="http://springerlink.metapress.com/content/h81468706x24/">Special
          Issue on User Interfaces for Theorem Proving</a>, Springer
        Netherlands, ISSN 0168-7433, <a href="http://springerlink.metapress.com/content/y4wt440q28136q47">pp.
-         109-139</a>, 2007
+         109-139</a>, 2007.
       </em>
     [[toggle id=id9 text="Abstract..."]] [[toggleable id=id9 text="""
     *Abstract:* Matita is a new, document-centric, tactic-based interactive theorem prover. This paper focuses on some of the distinctive features of the user interaction with Matita, mostly characterized by the organization of the library as a searchable knowledge base, the emphasis on a high-quality notational rendering, and the complex interplay between syntax, presentation, and semantics.
@@ -27,7 +27,7 @@
        6th International Conference on Mathematical Knowledge Management.
        Hagenberg, Austria -- 27-30 June 2007. <a href="http://www.springerlink.com/content/u10172854312/">LNAI
          4573</a>, Springer Berlin / Heidelberg, ISBN 978-3-540-73083-5, <a href="http://www.springerlink.com/content/87747204m4r45565/">pp.
-         381-392</a>, 2007
+         381-392</a>, 2007.
       </em>
     [[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].
@@ -38,7 +38,7 @@
        "The world's oldest and biggest XML conference".  <em>Award</em>: Winner
        of the <a href="http://2006.xmlconference.org/scholarship.html">XML
                Scholarship 2006</a> as best student paper.  Boston, MA --
-       December 5-7, 2006
+       December 5-7, 2006.
       </em>
     [[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.
@@ -49,7 +49,7 @@
          2006</a>: Types for Proofs and Programs. Nottingham, UK -- April
        18-21, 2006.  <a href="http://www.springerlink.com/content/u4h217614314/">LNCS
          4502</a>, Springer Berlin / Heidelberg, ISBN 978-3-540-74463-4, <a href="http://www.springerlink.com/content/148x29r15435650l/">pp.
-         18-32</a>, 2007
+         18-32</a>, 2007.
       </em>
     [[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.
@@ -71,7 +71,7 @@
        International Symposium on Wikis. Odense, Denmark -- August 21-23, 2006.
        ACM Press, 2006, ISBN 1-59593-417-0,
        <a href="http://www.wikisym.org/ws2006/proceedings/p89.pdf">pp.
-         89-98</a>
+         89-98</a>.
       </em>
     [[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.
@@ -82,7 +82,7 @@
          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
          4108</a>, Springer Berlin / Heidelberg, ISBN 978-3-540-37104-5, <a href="http://www.springerlink.com/content/h603702tj6306100/">pp.
-         194-207</a>, 2006
+         194-207</a>, 2006.
       </em>
     [[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.
@@ -94,7 +94,7 @@
        Proofs and Programs. Paris, France -- December 15-18, 2004.
        <a href="http://www.springerlink.com/content/978-3-540-31428-8/">LNCS
          3839</a>, Springer Berlin / Heidelberg, ISBN 3-540-31428-8, <a href="http://www.springerlink.com/content/y13172v735082217/">pp.
-         17-32</a>, 2006
+         17-32</a>, 2006.
       </em>
     [[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.
        <a href="http://www.springerlink.com/content/978-3-540-23580-4/">LNCS
          3286</a>, Springer Berlin / Heidelberg, ISBN 3-540-23580-9,
        <a href="http://www.springerlink.com/content/3cf6a7vvry9d1la1/">pp.
-         469-487</a>, 2004
+         469-487</a>, 2004.
       </em>
     [[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.
        In Proceedings of
        <a href="http://eic-ecm4.sub.uni-goettingen.de/">New Developments in
          Electronic Publishing of Mathematics 2004</a>.
-       Stockholm, Sweden -- June 2004. Edited by FIZ Karlsruhe, 2004
+       Stockholm, Sweden -- June 2004. Edited by FIZ Karlsruhe, 2004.
       </em>
     [[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.
        <a href="http://www.springerlink.com/content/978-3-540-23029-8/">LNCS
          3119</a>, Springer Berlin / Heidelberg, ISBN 3-540-23029-7,
        <a href="http://www.springerlink.com/content/kxkbpg34y5xrtenu/">pp.
-         347-362</a>, 2004
+         347-362</a>, 2004.
       </em>
     [[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.
          2003</a>
        11th Symposium on the Integration of Symbolic Computation and Mechanized
        Reasoning. Roma, Italy -- September 10-12, 2003, Aracne Editrice S.R.L.
-       ISBN 88-7999-545-6, pp. 43-57, 2003
+       ISBN 88-7999-545-6, pp. 43-57, 2003.
       </em>
     [[toggle id=id1 text="Abstract..."]] [[toggleable id=id1 text="""
     *Abstract:* We present a planning broker and several Web-Services for automatic deduction. Each Web-Service implements one of the tactics usually available in interactive proof-assistants. When the broker is submitted a proof status (an incomplete proof tree and a focus on an open goal) it dispatches the proof to the Web-Services, collects the successful results, and send them back to the client as hints as soon as they are available. In our experience this architecture turns out to be helpful both for experienced users (who can take benefit of distributing heavy computations) and beginners (who can learn from it).
 
  1. 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>)
+       by: <a href="http://www.cs.unibo.it/~busi">Nadia Busi</a>).
       </em>