more DOIs
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 6 Nov 2008 13:00:28 +0000 (14:00 +0100)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 6 Nov 2008 13:00:28 +0000 (14:00 +0100)
research/publications.mdwn

index 9df3b3c..881e680 100644 (file)
@@ -80,7 +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> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/978-3-540-73086-6_30" title="Document Object Identifier">doi&gt;</a></span> 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
@@ -100,7 +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> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/978-3-540-74464-1_2" title="Document Object Identifier">doi&gt;</a></span> 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
@@ -130,7 +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> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/11812289_16" title="Document Object Identifier">doi&gt;</a></span> 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
@@ -140,7 +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> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/11617990_2" title="Document Object Identifier">doi&gt;</a></span> 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.
@@ -151,7 +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> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/b101929" title="Document Object Identifier">doi&gt;</a></span> 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