helm/www/matita/papers.shtml

   1 <small>
   2   <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
   3 </small>
   4
   5 <ul>
   6   <li class="paper">
   7   <span class="paper_author">
   8     Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
   9   </span><br/>
  10   <span class="paper_title">
  11     A Bi-directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
  12   </span>
  13   <a class="paper_download" href="PAPERS/lmcs_types_2010.pdf">
  14     <span class="pdf_logo">.pdf</span>
  15   </a>
  16   <span class="paper_info">
  17     Published in Logical Methods in Computer Science, volume 8, Pages 1-49, 2012. DOI:10.2168/LMCS-8(1:18)2012. ISSN: 1860-5974.
  18   </span>
  19   <span class="paper_abstract">
  20     The paper describes the refinement algorithm for the Calculus of (Co)Inductive
  21     Constructions (CIC) implemented in the interactive theorem prover Matita.  The
  22     refinement algorithm is in charge of giving a meaning to the terms, types and
  23     proof terms directly written by the user or generated by using tactics,
  24     decision procedures or general automation. The terms are written in an
  25     “external syntax” meant to be user friendly that allows omission of
  26     information, untyped binders and a certain liberal use of user defined
  27     sub-typing. The refiner modifies the terms to obtain related well typed terms
  28     in the internal syntax understood by the kernel of the ITP. In particular, it
  29     acts as a type inference algorithm when all the binders are untyped.  The
  30     proposed algorithm is bi-directional: given a term in external syntax and a
  31     type expected for the term, it propagates as much typing information as
  32     possible towards the leaves of the term. Traditional mono-directional
  33     algorithms, instead, proceed in a bottom- up way by inferring the type of a
  34     sub-term and comparing (unifying) it with the type expected by its context only
  35     at the end. We propose some novel bi-directional rules for CIC that are
  36     particularly effective. Among the benefits of bi-directionality we have better
  37     error message reporting and better inference of dependent types. Moreover,
  38     thanks to bi-directionality, the coercion system for sub-typing is more
  39     effective and type inference generates simpler unification problems that are
  40     more likely to be solved by the inherently incomplete higher order unification
  41     algorithms implemented.  Finally we introduce in the external syntax the notion
  42     of vector of placeholders that enables to omit at once an arbitrary number of
  43     arguments. Vectors of placeholders allow a trivial implementation of implicit
  44     arguments and greatly simplify the implementation of primitive and simple
  45     tactics.
  46   </span>
  47   </li>
  48
  49   <li class="paper">
  50   <span class="paper_author">
  51     Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
  52   </span><br/>
  53   <span class="paper_title">
  54     The Matita Interactive Theorem Prover
  55   </span>
  56   <a class="paper_download" href="PAPERS/system_description2011.pdf">
  57     <span class="pdf_logo">.pdf</span>
  58   </a>
  59   <span class="paper_info">
  60     In Automated Deduction – CADE-23, LECTURE NOTES IN COMPUTER SCIENCE,
  61     ISBN:978-3-642-22437-9, Pages 64-69, Volume 6803, Year 2011 64-69.
  62   </span>
  63   </li>
  64
  65   <li class="paper">
  66   <span class="paper_author">
  67     Claudio Sacerdoti Coen, Enrico Tassi
  68   </span><br/>
  69   <span class="paper_title">
  70     Nonuniform Coercions via Unification Hints
  71   </span>
  72   <a class="paper_download" href="PAPERS/nonunifcoerc.pdf">
  73     <span class="pdf_logo">.pdf</span>
  74   </a>
  75   <span class="paper_info">
  76      In Proceedings Types for Proofs and Programs, Revised Selected Papers,
  77      ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE (EPTCS),
  78      ISSN:2075-2180, DOI:10.4204/EPTCS.53.2, vol. 53, 19-26, March 2011.
  79   </span>
  80   <span class="paper_abstract">
  81      We introduce the notion of nonuniform coercion, which is the promotion of a
  82      value of one type to an enriched value of a different type via a nonuniform
  83      procedure. Nonuniform coercions are a generalization of the (uniform) coercions
  84      known in the literature and they arise naturally when formalizing mathematics in
  85      an higher order interactive theorem prover using convenient devices like
  86      canonical structures, type classes or unification hints. We also show how
  87      nonuniform coercions can be naturally implemented at the user level in an
  88      interactive theorem prover that allows unification hints.
  89   </span>
  90   </li>
  91
  92   <li class="paper">
  93   <span class="paper_author">
  94     Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
  95   </span><br/>
  96   <span class="paper_title">
  97     Hints in Unification
  98   </span>
  99   <a class="paper_download" href="PAPERS/tphol09.pdf">
 100     <span class="pdf_logo">.pdf</span>
 101   </a>
 102   <span class="paper_info">
 103   In Proceedings of Theorem Proving in Higher Order Logics (TPHOLs 2009),
 104   Munich, August 17-20, 2009. LECTURE NOTES IN COMPUTER SCIENCE,
 105   ISBN:978-3-642-03358-2, vol. 5674. 84-98.
 106   </span>
 107   <span class="paper_abstract">
 108       Several mechanisms such as Canonical Structures, Type Classes, or
 109       Pullbacks have been recently introduced with the aim to improve the power
 110       and flexibility of the type inference algorithm for interactive theorem
 111       provers. We claim that all these mechanisms are particular instances of a
 112       simpler and more general technique, just consisting in providing suitable
 113       hints to the unification procedure underlying type inference. This allows
 114       a simple, modular and not intrusive implementation of all the above
 115       mentioned techniques, opening at the same time innovative and unexpected
 116       perspectives on its possible applications.
 117   </span>
 118   </li>
 119
 120   <li class="paper">
 121   <span class="paper_author">
 122     Andrea Asperti, Enrico Tassi
 123   </span><br/>
 124   <span class="paper_title">
 125     Smart Matching
 126   </span>
 127   <a class="paper_download" href="PAPERS/smart.pdf">
 128     <span class="pdf_logo">.pdf</span>
 129   </a>
 130   <span class="paper_info">
 131     Published in the proceedings of MKM2010, LNCS, Volume 6167/2010, Year 2010,
 132     Pages 263-277, DOI 10.1007/978-3-642-14128-7_23, ISBN 978-3-642-14127-0.
 133   </span>
 134   <span class="paper_abstract">
 135     One of the most annoying aspects in the formalization of
 136     mathematics is the need of transforming notions to match a given, existing
 137     result. This kind of transformations, often based on a conspicuous background
 138     knowledge in the given scientific domain (mostly expressed in the form of
 139     equalities or isomorphisms), are usually implicit in the mathematical
 140     discourse, and it would be highly desirable to obtain a similar behavior in
 141     interactive provers. The paper describes the superposition-based implementation
 142     of this feature inside the Matita interactive theorem prover, focusing in
 143     particular on the so called smart application tactic, supporting smart matching
 144     between a goal and a given result.
 145   </span>
 146   </li>
 147
 148   <li class="paper">
 149   <span class="paper_author">
 150     Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
 151   </span><br/>
 152   <span class="paper_title">
 153     A New Type For Tactics
 154   </span>
 155   <a class="paper_download" href="PAPERS/plmms09.pdf">
 156     <span class="pdf_logo">.pdf</span>
 157   </a>
 158   <span class="paper_info">
 159       To appear in the proceedings of ACM SIGSAM PLMMS 2009, ISBN 978-1-60558-735-6.
 160       Published as technical report UBLCS-2009-14.
 161   </span>
 162   <span class="paper_abstract">
 163     The type of tactics in all (procedural) proof assistants is (a variant of)
 164     the one introduced in LCF. We discuss why this is inconvenient and we
 165     propose
 166     a new type for tactics that 1) allows the implementation of more clever
 167     tactics; 2) improves the implementation of declarative languages on top
 168     of procedural ones; 3) allows for better proof structuring; 4) improves
 169     proof automation; 5) allows tactics to rearrange and delay the goals to be
 170     proved (e.g. in case of side conditions or PVS subtyping judgements).
 171   </span>
 172   </li>
 173
 174   <li class="paper">
 175   <span class="paper_author">
 176     Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
 177   </span><br/>
 178   <span class="paper_title">
 179     A Compact Kernel for the Calculus of Inductive Constructions
 180   </span>
 181   <a class="paper_download" href="PAPERS/sadhana.pdf">
 182     <span class="pdf_logo">.pdf</span>
 183   </a>
 184   <span class="paper_info">
 185     Published in the <a href="http://www.springer.com/engineering/journal/12046">Journal Sadhana</a>,
 186   </span>
 187   <span class="paper_abstract">
 188     The paper describes the new kernel for the Calculus of Inductive
 189     Constructions (CIC) implemented inside the Matita Interactive Theorem Prover.
 190     The design of the new kernel has been completely revisited since
 191     the first release, resulting in a remarkably compact implementation
 192     of about 2300 lines of OCaml code. The work is meant for people
 193     interested in implementation aspects of Interactive Provers, and
 194     is not self contained. In particular, it requires good
 195     acquaintance with Type Theory and functional programming languages.
 196   </span>
 197   </li>
 198
 199   <li class="paper">
 200   <span class="paper_author">
 201     Andrea Asperti, Enrico Tassi
 202   </span><br/>
 203   <span class="paper_title">
 204     Higher order proof reconstruction from paramodulation-based refutations:
 205     the unit equality case
 206   </span>
 207   <a class="paper_download" href="PAPERS/hopr.pdf">
 208     <span class="pdf_logo">.pdf</span>
 209   </a>
 210   <span class="paper_info">
 211     Accepted for publication in the proceedings of MKM 2007: The 6th
 212     International Conference on Mathematical Knowledge Management.
 213   </span>
 214   <span class="paper_abstract">
 215     In this paper we address the problem of reconstructing a
 216     higher order, checkable proof object starting from a proof trace left by a
 217     first order automatic proof searching procedure, in a restricted equational
 218     framework. The automatic procedure is based on superposition rules for
 219     the unit equality case. Proof transformation techniques aimed to improve
 220     the readability of the final proof are discussed.
 221   </span>
 222   </li>
 223
 224   <li class="paper">
 225   <span class="paper_author">
 226     Claudio Sacerdoti Coen, Stefano Zacchiroli
 227   </span><br/>
 228   <span class="paper_title">
 229     Spurious Disambiguation Error Detection
 230   </span>
 231   <a class="paper_download" href="PAPERS/disambiguation-errors.pdf">
 232     <span class="pdf_logo">.pdf</span>
 233   </a>
 234   <span class="paper_info">
 235     Accepted for publication in the proceedings of MKM 2007: The 6th
 236     International Conference on Mathematical Knowledge Management.
 237   </span>
 238   <span class="paper_abstract">
 239     The disambiguation approach to the input of formulae enables the user to
 240     type correct formulae in a terse syntax close to the usual ambiguous
 241     mathematical notation. When it comes to incorrect formulae we want to
 242     present only errors related to the interpretation meant by the user, hiding
 243     errors related to other interpretations (spurious errors). We propose a
 244     heuristic to recognize spurious errors, which has been integrated with our
 245     former efficient disambiguation algorithm.
 246   </span>
 247   </li>
 248
 249   <li class="paper">
 250   <span class="paper_author">
 251     Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
 252   </span><br/>
 253   <span class="paper_title">
 254     Crafting a Proof Assistant
 255   </span>
 256   <a class="paper_download" href="PAPERS/matita_types.pdf">
 257     <span class="pdf_logo">.pdf</span>
 258   </a>
 259   <span class="paper_info">
 260     Accepted for publication in the Proceedings of Types 2006: Conference of
 261     the Types Project. Nottingham, UK -- April 18-21, 2006.
 262   </span>
 263   <span class="paper_abstract">
 264      Proof assistants are complex applications whose develop-
 265      ment has never been properly systematized or documented. This work is
 266      a contribution in this direction, based on our experience with the devel-
 267      opment of Matita: a new interactive theorem prover based—as Coq—on
 268      the Calculus of Inductive Constructions (CIC). In particular, we analyze
 269      its architecture focusing on the dependencies of its components, how they
 270      implement the main functionalities, and their degree of reusability.
 271      The work is a first attempt to provide a ground for a more direct com-
 272      parison between different systems and to highlight the common func-
 273      tionalities, not only in view of reusability but also to encourage a more
 274      systematic comparison of different softwares and architectural solutions.
 275   </span>
 276   </li>
 277
 278
 279   <li class="paper">
 280   <span class="paper_author">
 281     Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
 282   </span><br/>
 283   <span class="paper_title">
 284     User Interaction with the Matita Proof Assistant
 285   </span>
 286   <a class="paper_download" href="PAPERS/matita.pdf">
 287     <span class="pdf_logo">.pdf</span>
 288   </a>
 289   <span class="paper_info">
 290     Accepted for publication in Journal of Automated Reasoning, Special Issue
 291     on User Interfaces for Theorem Proving.
 292   </span>
 293   <span class="paper_abstract">
 294      Matita is a new, document-centric, tactic-based interactive theorem
 295      prover. This paper focuses on some of the distinctive features of the user interaction
 296      with Matita, mostly characterized by the organization of the library as a search-
 297      able knowledge base, the emphasis on a high-quality notational rendering, and the
 298      complex interplay between syntax, presentation, and semantics.
 299   </span>
 300   </li>
 301
 302
 303   <li class="paper">
 304   <span class="paper_author">
 305     Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
 306   </span><br/>
 307   <span class="paper_title">
 308       Tinycals: step by step tacticals
 309   </span>
 310   <a class="paper_download" href="PAPERS/tinycals.pdf">
 311     <span class="pdf_logo">.pdf</span>
 312   </a>
 313   <span class="paper_info">
 314     In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle,
 315     WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 -
 316     142, ISSN:1571-0661
 317   </span>
 318   <span class="paper_abstract">
 319       Most of the state-of-the-art proof assistants are based on procedural
 320       proof languages, scripts, and rely on LCF tacticals as the primary tool
 321       for tactics composition. In this paper we discuss how these ingredients
 322       do not interact well with user interfaces based on the same interaction
 323       paradigm of Proof General (the de facto standard in this field),
 324       identifying in the coarse-grainedness of tactical evaluation the key
 325       problem.
 326
 327       We propose tinycals as an alternative to a subset of LCF tacticals,
 328       showing that the user does not experience the same problem if tacticals
 329       are evaluated in a more fine-grained manner. We present the formal
 330       operational semantics of tinycals as well as their implementation in the
 331       Matita proof assistant.
 332   </span>
 333   </li>
 334
 335
 336   <li class="paper">
 337   <span class="paper_author">Luca Padovani, Stefano Zacchiroli</span><br/>
 338   <span class="paper_title">
 339       From notation to semantics: there and back again
 340   </span>
 341   <a class="paper_download" href="PAPERS/notation.pdf">
 342     <span class="pdf_logo">.pdf</span>
 343   </a>
 344   <span class="paper_info">
 345       Accepted for publication in the proceedings of MKM 2006: The 5th
 346       International Conference on Mathematical Knowledge Management.
 347       Wokingham, UK -- August 11-12, 2006.
 348   </span>
 349   <span class="paper_abstract">
 350       Mathematical notation is a structured, open, and ambiguous language.  In
 351       order to support mathematical notation in MKM applications one must
 352       necessarily take into account presentational as well as semantic aspects.
 353       The former are required to create a familiar, comfortable, and usable
 354       interface to interact with.  The latter are necessary in order to process
 355       the information meaningfully.  In this paper we investigate a framework
 356       for dealing with mathematical notation in a meaningful, extensible way,
 357       and we show an effective instantiation of its architecture to the field
 358       of interactive theorem proving. The framework builds upon well-known
 359       concepts and widely-used technologies and it can be easily adopted by
 360       other MKM applications.
 361   </span>
 362   </li>
 363
 364
 365   <li class="paper">
 366   <span class="paper_author">
 367     Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
 368   </span><br/>
 369   <span class="paper_title">
 370       A content based mathematical search engine: Whelp
 371   </span>
 372   <a class="paper_download" href="PAPERS/whelp.pdf">
 373     <span class="pdf_logo">.pdf</span>
 374   </a>
 375   <span class="paper_info">
 376       In Proceedings of TYPES 2004 conference Types for Proofs and Programs.
 377       Paris, France -- December 15-18, 2004.  LNCS 3839/2004, Springer-Verlag
 378       Heidelberg, ISBN 3-540-31428-8, pp. 17-32
 379   </span>
 380   <span class="paper_abstract">
 381       The prototype of a content based search engine for mathematical knowledge
 382       supporting a small set of queries requiring matching and/or typing
 383       operations is described. The prototype, called Whelp, exploits a metadata
 384       approach for indexing the information that looks far more flexible than
 385       traditional indexing techniques for structured expressions like
 386       substitution, discrimination, or context trees. The prototype has been
 387       instantiated to the standard library of the Coq proof assistant extended
 388       with many user contributions.
 389   </span>
 390   </li>
 391
 392
 393   <li class="paper">
 394   <span class="paper_author">
 395     Claudio Sacerdoti Coen, Stefano Zacchiroli
 396   </span><br/>
 397   <span class="paper_title">
 398     Efficient Ambiguous Parsing of Mathematical Formulae
 399   </span>
 400   <a class="paper_download" href="PAPERS/disambiguation.pdf">
 401     <span class="pdf_logo">.pdf</span>
 402   </a>
 403   <span class="paper_info">
 404       In Proceedings of MKM 2004
 405       Third International Conference on Mathematical Knowledge Management.
 406       September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
 407       Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
 408   </span>
 409   <span class="paper_abstract">
 410       Mathematical notation has the characteristic of being ambiguous:
 411       operators can be overloaded and information that can be deduced is often
 412       omitted.  Mathematicians are used to this ambiguity and can easily
 413       disambiguate a formula making use of the context and of their ability to
 414       find the right interpretation.
 415
 416       Software applications that have to deal with formulae usually avoid these
 417       issues by fixing an unambiguous input notation. This solution is annoying
 418       for mathematicians because of the resulting tricky syntaxes and becomes a
 419       show stopper to the simultaneous adoption of tools characterized by
 420       different input languages.
 421
 422       In this paper we present an efficient algorithm suitable for ambiguous
 423       parsing of mathematical formulae. The only requirement of the algorithm
 424       is the existence of a validity predicate over abstract syntax trees of
 425       incomplete formulae with placeholders. This requirement can be easily
 426       fulfilled in the applicative area of interactive proof assistants, and in
 427       several other areas of Mathematical Knowledge Management.
 428   </span>
 429   </li>
 430
 431 </ul>