more fine grained classification for publications
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 15 Mar 2011 09:41:41 +0000 (10:41 +0100)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 15 Mar 2011 09:41:41 +0000 (10:41 +0100)
research/publications.mdwn
research/publications/studia11-dh-ocaml.pdf [new file with mode: 0644]

index 3a08317..33ac227 100644 (file)
@@ -5,7 +5,7 @@ Here is a list of my **academic papers**, classified by type of publication and
 in reverse chronological order.
 [[!toc ]]
 
-# <span title="international, peer-reviewed journals">journal articles</span>
+# <span title="international, peer-reviewed journals">international, peer-reviewed journal articles</span>
 
  1. <a class="paper_download" href="scp2010-evolution.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1016/j.scico.2010.11.001" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.di.univaq.it/diruscio/">Davide Di Ruscio</a>, <a href="http://www.di.univaq.it/pellicci/">Patrizio Pelliccione</a>, <a href="http://www.di.univaq.it/alfonso/">Alfonso Pierantonio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Supporting Software Evolution in Component-Based FOSS Systems**.  <em>Article in press, to appear in<a href="http://www.elsevier.com/locate/scico/">Science of Computer
       Programming</a>, ISSN 0167-6423. Elsevier, 2010.</em>
@@ -39,7 +39,7 @@ in reverse chronological order.
     *Abstract:* A foreseeable incarnation of Web 3.0 could inherit machine understandability from the Semantic Web, and collaborative editing from Web 2.0 applications. We review the research and development trends which are getting today Web nearer to such an incarnation. We present semantic wikis, microformats, and the so-called "lowercase semantic web": they are the main approaches at closing the technological gap between content authors and Semantic Web technologies. We discuss a too often neglected aspect of the associated technologies, namely how much they adhere to the wiki philosophy of open editing: is there an intrinsic incompatibility between semantic rich content and unconstrained editing? We argue that the answer to this question can be "no", provided that a few yet relevant shortcomings of current Web technologies will be fixed soon.
     """]]
 
-# <span title="international, peer-reviewed conferences">conference proceedings</span>
+# <span title="international, peer-reviewed conferences">international, peer-reviewed conference proceedings</span>
 
  1. Pietro Abate, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **MPM: a modular package manager**.  <em>To appear in proceedings of CBSE 2011 (the<a href="http://cbse-conferences.org/2011/">14th International ACM SIGSOFT
       Symposium on Component Based Software Engineering</a>), Boulder, Colorado, USA, 21-23 June, 2011.</em>
@@ -52,33 +52,12 @@ in reverse chronological order.
     [[!toggle id=id34 text="Abstract..."]] [[!toggleable id=id34 text="""
     *Abstract:* FOSS (Free and Open Source Software) distributions use dependencies and package managers to maintain huge collections of packages and their installations; recent research have led to efficient and complete configuration tools and techniques, based on state of the art solvers, that are being adopted in industry. We show how to encode a significant subset of Free Feature Diagrams as interdependent packages, enabling to reuse package tools and research results into software product lines.
     """]]
- 1. <a class="paper_download" href="msr2010-udd.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1109/MSR.2010.5463277" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.loria.fr/~lnussbau/">Lucas Nussbaum</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **The Ultimate Debian Database: Consolidating Bazaar Metadata for Quality Assurance and Data Mining**.  <em>In<a href="http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5457933">proceedings
-      of MSR 2010</a>(the<a href="http://msr.uwaterloo.ca/msr2010/">7th IEEE
-      Working Conference on Mining Software Repositories</a>, co-located with<a href="http://www.sbs.co.za/ICSE2010/">ICSE 2010</a>), IEEE, ISBN 978-1-4244-6802-7,<a href="http://ieeexplore.ieee.org/search/srchabstract.jsp?tp=&amp;arnumber=5463277">pp. 52-61</a>. 02-03/05/2010, Cape Town, South Africa.</em>
-    [[!toggle id=id33 text="Abstract..."]] [[!toggleable id=id33 text="""
-    *Abstract:* FLOSS distributions like RedHat and Ubuntu require a lot more complex infrastructures than most other FLOSS projects. In the case of community-driven distributions like Debian, the development of such an infrastructure is often not very organized, leading to new data sources being added in an impromptu manner while hackers set up new services that gain acceptance in the community. Mixing and matching data is then harder than should be, albeit being badly needed for Quality Assurance and data mining. Massive refactoring and integration is not a viable solution either, due to the constraints imposed by the bazaar development model. This paper presents the Ultimate Debian Database (UDD), which is the countermeasure adopted by the Debian project to the above "data hell". UDD gathers data from various data sources into a single, central SQL database, turning Quality Assurance needs that could not be easily implemented before into simple SQL queries. The paper also discusses the customs that have contributed to the data hell, the lessons learnt while designing UDD, and its applications and potentialities for data mining on FLOSS distributions.
-    """]]
- 1. <a class="paper_download" href="jfla10-dh-ocaml.pdf">[.pdf]</a> <a href="http://www.pps.jussieu.fr/~dogguy/">Mehdi Dogguy</a>, <a href="http://stephane.glondu.net/">Stéphane Glondu</a>, <a href="http://sylvain.le-gall.net/">Sylvain Le Gall</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Enforcing Type-Safe Linking using Inter-Package Relationships**.  <em>In proceedings of JFLA 2010 (the<a href="http://jfla.inria.fr/2010/">21st Journée Francophones des Langages
-      Applicatifs</a>), pp. 29-54. 30/01-02/02/2010 - La Ciotat, France.</em>
-    [[!toggle id=id32 text="Abstract..."]] [[!toggleable id=id32 text="""
-    *Abstract:* Strongly-typed languages rely on link-time checks to ensure that type safety is not violated at the borders of compilation units. Such checks entail very fine-grained dependencies among compilation units, which are at odds with the implicit assumption of backward compatibility that is relied upon by common library packaging techniques adopted by FOSS (Free and Open Source Software) package-based distributions. As a consequence, package managers are often unable to prevent users to install a set of libraries which cannot be linked together. We discuss how to guarantee link-time compatibility using inter-package relationships; in doing so, we take into account real-life maintainability problems such as support for automatic package rebuild and manageability of ABI (Application Binary Interface) strings by humans. We present the dh_ocaml implementation of the proposed solution, which is currently in use in the Debian distribution to safely deploy more than 300 OCaml-related packages.
-    """]]
  1. <a class="paper_download" href="sac10-coclo.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1774088.1774259" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.cs.unibo.it/~gdangelo/">Gabriele D'Angelo</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Content Cloaking: Preserving Privacy with Google Docs and other Web Applications**.  <em>In<a href="http://portal.acm.org/toc.cfm?id=1774088&amp;type=proceeding&amp;coll=GUIDE&amp;dl=GUIDE&amp;CFID=106564825&amp;CFTOKEN=63108649">proceedings
       of ACM SAC 2010</a>(the<a href="http://www.acm.org/conferences/sac/sac2010/">25th Annual ACM
       Symposium on Applied Computing</a>), ISBN 978-1-60558-639-7,<a href="http://portal.acm.org/citation.cfm?doid=1774088.1774259">pp. 826-830</a>. 22-26/03/2010 - Sierre, Switzerland.</em>
     [[!toggle id=id31 text="Abstract..."]] [[!toggleable id=id31 text="""
     *Abstract:* Web office suites such as Google Docs offer unparalleled collaboration experiences in terms of low software requirements, ease of use, data ubiquity, and availability. When the data holder (Google, Microsoft, etc.) is not perceived as trusted though, those benefits are considered at stake with important privacy requirements. Content cloaking is a lightweight, cryptographic, client-side solution to protect content from data holders while using web office suites and other "Web 2.0", AJAX-based, collaborative applications.
     """]]
- 1. <a class="paper_download" href="mooml-iwoce-2009.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1595800.1595806" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Expressing Advanced User preferences in Component Installation**.  <em>In proceedings of<a href="http://www.iwoce.org">IWOCE 2009</a>International Workshop on Open Component Ecosystem, affiliated with<a href="http://www.esec-fse-2009.ewi.tudelft.nl/">ESEC/FSE
-       2009</a>. Foundations of Software Engineering, ISBN 978-1-60558-677-9,<a href="http://portal.acm.org/citation.cfm?id=1595800.1595806">pp. 31-40</a>, ACM 2009.</em>
-    [[!toggle id=id30 text="Abstract..."]] [[!toggleable id=id30 text="""
-    *Abstract:* State of the art component-based software collections, such as FOSS distributions, are made of up to dozens of thousands components, with complex inter-dependencies and conflicts. Given a particular installation of such a system, each request to alter the set of installed components has potentially (too) many satisfying answers. We present an architecture that allows to express advanced user preferences about package selection in FOSS distributions. The architecture is composed by a distribution-independent format for describing available and installed packages called CUDF (Common Upgradeability Description Format), and a foundational language called MooML to specify optimization criteria. We present the syntax and semantics of CUDF and MooML, and discuss the partial evaluation mechanism of MooML which allows to gain efficiency in package dependency solvers.
-    """]]
- 1. <a class="paper_download" href="modernization-iwoce-2009.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1595800.1595803" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.di.univaq.it/diruscio/">Davide Di Ruscio</a>, <a href="http://www.di.univaq.it/pellicci/">Patrizio Pelliccione</a>, <a href="http://www.di.univaq.it/alfonso/">Alfonso Pierantonio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Towards maintainer script modernization in FOSS distributions**.  <em>In proceedings of<a href="http://www.iwoce.org">IWOCE 2009</a>International Workshop on Open Component Ecosystem, affiliated with<a href="http://www.esec-fse-2009.ewi.tudelft.nl/">ESEC/FSE
-       2009</a>. Foundations of Software Engineering, ISBN 978-1-60558-677-9,<a href="http://portal.acm.org/citation.cfm?id=1595800.1595803">pp. 11-20</a>, ACM 2009.</em>
-    [[!toggle id=id29 text="Abstract..."]] [[!toggleable id=id29 text="""
-    *Abstract:* Free and Open Source Software (FOSS) distributions are complex software systems, made of thousands packages that evolve rapidly, independently, and without centralized coordination. During packages upgrades, corner case failures can be encountered and are hard to deal with, especially when they are due to misbehaving maintainer scripts: executable code snippets used to finalize package configuration. In this paper we report a software modernization experience, the process of representing existing legacy systems in terms of models, applied to FOSS distributions. We present a process to define meta-models that enable dealing with upgrade failures and help rolling back from them, taking into account maintainer scripts. The process has been applied to widely used FOSS distributions and we report about such experiences.
-    """]]
  1. <a class="paper_download" href="strongdeps-esem-2009.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1109/ESEM.2009.5316017" title="Document Object Identifier">doi&gt;</a></span> Pietro Abate, Jaap Boender, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Strong Dependencies between Software Components**.  <em>In proceedings of<a href="http://www.csc2.ncsu.edu/conferences/esem/">ESEM 2009</a>(3rd International Symposium on Empirical Software Engineering and Measurement), ISBN 978-1-4244-4842-5,<a href="http://ieeexplore.ieee.org/search/wrapper.jsp?arnumber=5316017">pp. 89-99</a>. October 15-16, 2009 - Lake Buena Vista, Florida, USA.</em>
     [[!toggle id=id28 text="Abstract..."]] [[!toggleable id=id28 text="""
     *Abstract:* Component-based systems often describe context requirements in terms of explicit inter-component dependencies. Studying large instances of such systems—such as free and open source software (FOSS) distributions—in terms of declared dependencies between packages is appealing. It is however also misleading when the language to express dependencies is as expressive as boolean formulae, which is often the case. In such settings, a more appropriate notion of component dependency exists: strong dependency. This paper introduces such notion as a first step towards modeling semantic, rather then syntactic, inter-component relationships. Furthermore, a notion of component sensitivity is derived from strong dependencies, with applications to quality assurance and to the evaluation of upgrade risks. An empirical study of strong dependencies and sensitivity is presented, in the context of one of the largest, freely available, component-based system.
@@ -93,32 +72,17 @@ 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">[.pdf]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1490283.1490292" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://paulotrezentos.polo-sul.org/">Paulo Trezentos</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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.</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">[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1145/1367497.1367581" title="Document Object Identifier">doi&gt;</a></span> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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,<a href="http://portal.acm.org/citation.cfm?doid=1367497.1367581">pp.
           615-624</a>.</em>
     [[!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">[.pdf]</a> <a href="http://vitali.web.cs.unibo.it/Main/PaoloMarinelli">Paolo Marinelli</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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=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">[.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> <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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=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">[.pdf]</a> <a href="http://vitali.web.cs.unibo.it/Main/PaoloMarinelli">Paolo Marinelli</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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=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">[.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> <a href="http://www.cs.unibo.it/~asperti">Andrea Asperti</a>, <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://www.cs.unibo.it/~tassi">Enrico Tassi</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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
          4502</a>, Springer Berlin / Heidelberg, ISBN 978-3-540-74463-4,<a href="http://www.springerlink.com/content/148x29r15435650l/">pp.
@@ -126,16 +90,6 @@ 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">[.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> <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://www.cs.unibo.it/~tassi">Enrico Tassi</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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 21, 2006.<a href="http://www.elsevier.com/locate/issn/15710661">ENTCS (Elsevier, ISSN 1571-0661)</a>,<a href="http://www.sciencedirect.com/science/journal/15710661">Volume 174, Issue 2, pp. 125-142 (15 May 2007)</a>.</em>
-    [[!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">[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1145/1149453.1149471" title="Document Object Identifier">doi&gt;</a></span> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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. ACM Press, 2006, ISBN 1-59593-417-0,<a href="http://www.wikisym.org/ws2006/proceedings/p89.pdf">pp.
-         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.
-    """]]
  1. <a class="paper_download" href="notation.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1007/11812289_16" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.sti.uniurb.it/padovani/">Luca Padovani</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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
          4108</a>, Springer Berlin / Heidelberg, ISBN 978-3-540-37104-5,<a href="http://www.springerlink.com/content/h603702tj6306100/">pp.
@@ -167,12 +121,71 @@ 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.
     """]]
+
+# <span title="international, peer-reviewed workshops">international, peer-reviewed workshop proceedings</span>
+
+ 1. <a class="paper_download" href="msr2010-udd.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1109/MSR.2010.5463277" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.loria.fr/~lnussbau/">Lucas Nussbaum</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **The Ultimate Debian Database: Consolidating Bazaar Metadata for Quality Assurance and Data Mining**.  <em>In<a href="http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5457933">proceedings
+      of MSR 2010</a>(the<a href="http://msr.uwaterloo.ca/msr2010/">7th IEEE
+      Working Conference on Mining Software Repositories</a>, co-located with<a href="http://www.sbs.co.za/ICSE2010/">ICSE 2010</a>), IEEE, ISBN 978-1-4244-6802-7,<a href="http://ieeexplore.ieee.org/search/srchabstract.jsp?tp=&amp;arnumber=5463277">pp. 52-61</a>. 02-03/05/2010, Cape Town, South Africa.</em>
+    [[!toggle id=id33 text="Abstract..."]] [[!toggleable id=id33 text="""
+    *Abstract:* FLOSS distributions like RedHat and Ubuntu require a lot more complex infrastructures than most other FLOSS projects. In the case of community-driven distributions like Debian, the development of such an infrastructure is often not very organized, leading to new data sources being added in an impromptu manner while hackers set up new services that gain acceptance in the community. Mixing and matching data is then harder than should be, albeit being badly needed for Quality Assurance and data mining. Massive refactoring and integration is not a viable solution either, due to the constraints imposed by the bazaar development model. This paper presents the Ultimate Debian Database (UDD), which is the countermeasure adopted by the Debian project to the above "data hell". UDD gathers data from various data sources into a single, central SQL database, turning Quality Assurance needs that could not be easily implemented before into simple SQL queries. The paper also discusses the customs that have contributed to the data hell, the lessons learnt while designing UDD, and its applications and potentialities for data mining on FLOSS distributions.
+    """]]
+ 1. <a class="paper_download" href="mooml-iwoce-2009.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1595800.1595806" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.pps.jussieu.fr/~treinen">Ralf Treinen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Expressing Advanced User preferences in Component Installation**.  <em>In proceedings of<a href="http://www.iwoce.org">IWOCE 2009</a>International Workshop on Open Component Ecosystem, affiliated with<a href="http://www.esec-fse-2009.ewi.tudelft.nl/">ESEC/FSE
+       2009</a>. Foundations of Software Engineering, ISBN 978-1-60558-677-9,<a href="http://portal.acm.org/citation.cfm?id=1595800.1595806">pp. 31-40</a>, ACM 2009.</em>
+    [[!toggle id=id30 text="Abstract..."]] [[!toggleable id=id30 text="""
+    *Abstract:* State of the art component-based software collections, such as FOSS distributions, are made of up to dozens of thousands components, with complex inter-dependencies and conflicts. Given a particular installation of such a system, each request to alter the set of installed components has potentially (too) many satisfying answers. We present an architecture that allows to express advanced user preferences about package selection in FOSS distributions. The architecture is composed by a distribution-independent format for describing available and installed packages called CUDF (Common Upgradeability Description Format), and a foundational language called MooML to specify optimization criteria. We present the syntax and semantics of CUDF and MooML, and discuss the partial evaluation mechanism of MooML which allows to gain efficiency in package dependency solvers.
+    """]]
+ 1. <a class="paper_download" href="modernization-iwoce-2009.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1595800.1595803" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.di.univaq.it/diruscio/">Davide Di Ruscio</a>, <a href="http://www.di.univaq.it/pellicci/">Patrizio Pelliccione</a>, <a href="http://www.di.univaq.it/alfonso/">Alfonso Pierantonio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Towards maintainer script modernization in FOSS distributions**.  <em>In proceedings of<a href="http://www.iwoce.org">IWOCE 2009</a>International Workshop on Open Component Ecosystem, affiliated with<a href="http://www.esec-fse-2009.ewi.tudelft.nl/">ESEC/FSE
+       2009</a>. Foundations of Software Engineering, ISBN 978-1-60558-677-9,<a href="http://portal.acm.org/citation.cfm?id=1595800.1595803">pp. 11-20</a>, ACM 2009.</em>
+    [[!toggle id=id29 text="Abstract..."]] [[!toggleable id=id29 text="""
+    *Abstract:* Free and Open Source Software (FOSS) distributions are complex software systems, made of thousands packages that evolve rapidly, independently, and without centralized coordination. During packages upgrades, corner case failures can be encountered and are hard to deal with, especially when they are due to misbehaving maintainer scripts: executable code snippets used to finalize package configuration. In this paper we report a software modernization experience, the process of representing existing legacy systems in terms of models, applied to FOSS distributions. We present a process to define meta-models that enable dealing with upgrade failures and help rolling back from them, taking into account maintainer scripts. The process has been applied to widely used FOSS distributions and we report about such experiences.
+    """]]
+ 1. <a class="paper_download" href="hotswup-package-upgrade.pdf">[.pdf]</a> <span class="doi_logo"><a href="http://doi.acm.org/10.1145/1490283.1490292" title="Document Object Identifier">doi&gt;</a></span> <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://paulotrezentos.polo-sul.org/">Paulo Trezentos</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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.</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="steve-latvia.pdf">[.pdf]</a> <a href="http://vitali.web.cs.unibo.it/Main/PaoloMarinelli">Paolo Marinelli</a>, <a href="http://vitali.web.cs.unibo.it">Fabio Vitali</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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=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="streaming-co-constraints.pdf">[.pdf]</a> <a href="http://vitali.web.cs.unibo.it/Main/PaoloMarinelli">Paolo Marinelli</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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=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="tinycals.pdf">[.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> <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://www.cs.unibo.it/~tassi">Enrico Tassi</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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 21, 2006.<a href="http://www.elsevier.com/locate/issn/15710661">ENTCS (Elsevier, ISSN 1571-0661)</a>,<a href="http://www.sciencedirect.com/science/journal/15710661">Volume 174, Issue 2, pp. 125-142 (15 May 2007)</a>.</em>
+    [[!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">[.pdf]</a> <span class="doi_logo"><a href="http://dx.doi.org/10.1145/1149453.1149471" title="Document Object Identifier">doi&gt;</a></span> <a href="http://diiorio.web.cs.unibo.it/">Angelo Di Iorio</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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. ACM Press, 2006, ISBN 1-59593-417-0,<a href="http://www.wikisym.org/ws2006/proceedings/p89.pdf">pp.
+         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.
+    """]]
  1. <a class="paper_download" href="hbugs.pdf">[.pdf]</a> <a href="http://www.cs.unibo.it/~sacerdot">Claudio Sacerdoti Coen</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **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>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.</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).
     """]]
 
+# <span title="national, peer-reviewed journals">national, peer-reviewed journal articles</span>
+
+ 1. <a class="paper_download" href="studia11-dh-ocaml.pdf">[.pdf]</a> <a href="http://www.pps.jussieu.fr/~dogguy/">Mehdi Dogguy</a>, <a href="http://stephane.glondu.net/">Stéphane Glondu</a>, <a href="http://sylvain.le-gall.net/">Sylvain Le Gall</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Enforcing Type-Safe Linking using Inter-Package Relationships**.  <em>Article in press, to appear in<a href="http://studia.complexica.net/">Studia Informatica Universalis</a>, Hermann.</em>
+    [[!toggle id=id37 text="Abstract..."]] [[!toggleable id=id37 text="""
+    *Abstract:* Strongly-typed languages rely on link-time checks to ensure that type safety is not violated at the borders of compilation units. Such checks entail very fine-grained dependencies among compilation units, which are at odds with the implicit assumption of backward compatibility that is relied upon by common library packaging techniques adopted by FOSS (Free and Open Source Software) package-based distributions. As a consequence, package managers are often unable to prevent users to install a set of libraries which cannot be linked together. We discuss how to guarantee link-time compatibility using inter-package relationships; in doing so, we take into account real-life maintainability problems such as support for automatic package rebuild and manageability of ABI (Application Binary Interface) strings by humans. We present the dh_ocaml implementation of the proposed solution, which is currently in use in the Debian distribution to safely deploy more than 300 OCaml-related packages.
+    """]]
+
+# <span title="national, peer-reviewed conferences and workshops">national, peer-reviewed conference and workshop procedings</span>
+
+ 1. <a class="paper_download" href="jfla10-dh-ocaml.pdf">[.pdf]</a> <a href="http://www.pps.jussieu.fr/~dogguy/">Mehdi Dogguy</a>, <a href="http://stephane.glondu.net/">Stéphane Glondu</a>, <a href="http://sylvain.le-gall.net/">Sylvain Le Gall</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Enforcing Type-Safe Linking using Inter-Package Relationships**.  <em>In proceedings of JFLA 2010 (the<a href="http://jfla.inria.fr/2010/">21st Journée Francophones des Langages
+      Applicatifs</a>), pp. 29-54. 30/01-02/02/2010 - La Ciotat, France.</em>
+    [[!toggle id=id32 text="Abstract..."]] [[!toggleable id=id32 text="""
+    *Abstract:* Strongly-typed languages rely on link-time checks to ensure that type safety is not violated at the borders of compilation units. Such checks entail very fine-grained dependencies among compilation units, which are at odds with the implicit assumption of backward compatibility that is relied upon by common library packaging techniques adopted by FOSS (Free and Open Source Software) package-based distributions. As a consequence, package managers are often unable to prevent users to install a set of libraries which cannot be linked together. We discuss how to guarantee link-time compatibility using inter-package relationships; in doing so, we take into account real-life maintainability problems such as support for automatic package rebuild and manageability of ABI (Application Binary Interface) strings by humans. We present the dh_ocaml implementation of the proposed solution, which is currently in use in the Debian distribution to safely deploy more than 300 OCaml-related packages.
+    """]]
+
 # <span title="official research reports of research institutions">technical reports</span>
 
  1. <a class="paper_download" href="strongdeps-tr.pdf">[.pdf]</a> Pietro Abate, Jaap Boender, <a href="http://www.dicosmo.org">Roberto Di Cosmo</a>, <a href="http://upsilon.cc/~zack">Stefano Zacchiroli</a>. **Strong Dependencies between Software Components**.  <em><a href="http://www.mancoosi.org">Mancoosi project</a><a href="http://www.mancoosi.org/reports/">technical report
diff --git a/research/publications/studia11-dh-ocaml.pdf b/research/publications/studia11-dh-ocaml.pdf
new file mode 100644 (file)
index 0000000..c7479f1
Binary files /dev/null and b/research/publications/studia11-dh-ocaml.pdf differ