web commit by zack
authorStefano Zacchiroli <zack@fettunta.org>
Thu, 20 Dec 2007 16:26:33 +0000 (16:26 +0000)
committerStefano Zacchiroli <zack@fettunta.org>
Thu, 20 Dec 2007 16:26:33 +0000 (16:26 +0000)
research/publications.mdwn

index 1de96fa..f763168 100644 (file)
@@ -7,17 +7,40 @@
         Netherlands, ISSN 0168-7433, <a href="http://springerlink.metapress.com/content/y4wt440q28136q47">pp.
           109-139</a>, 2007
       </em>
-    [[toggle id=matita text="abstract"]] [[toggleable id=matita text="""
-    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.
+    [[toggle id=matita text="Abstract."]] [[toggleable id=matita 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.
     """]]
 
-
 ## conference proceedings
 
- 1.  Paolo Marinelli, Fabio Vitali, Stefano Zacchiroli. **Streaming Validation of Schemata: the Lazy Typing Discipline**. <em>
+ 1. 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.
-      </em> [[toggle id=steve-latvia text="abstract"]] [[toggleable id=steve-latvia text="""
-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."""]]
+      </em>
+    [[toggle id=steve-latvia text="Abstract."]] [[toggleable id=steve-latvia 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. 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
+          4573</a>, Springer Berlin / Heidelberg, ISBN 978-3-540-73083-5, <a href="http://www.springerlink.com/content/87747204m4r45565/">pp.
+          381-392</a>, 2007
+      </em>
+    [[toggle id=disambiguation-errors text="Abstract."]] [[toggleable id=disambiguation-errors 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. 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
+                Scholarship 2006</a> as best student paper.  Boston, MA --
+        December 5-7, 2006
+      </em>
+    [[toggle id=streaming-co-constraints text="Abstract."]] [[toggleable id=streaming-co-constraints 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.
+    """]]