+<small>
+ <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
+</small>
+
<ul>
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ A Bi-directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
+ </span>
+ <a class="paper_download" href="PAPERS/lmcs_types_2010.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Published in Logical Methods in Computer Science, volume 8, Pages 1-49, 2012. DOI:10.2168/LMCS-8(1:18)2012. ISSN: 1860-5974.
+ </span>
+ <span class="paper_abstract">
+ The paper describes the refinement algorithm for the Calculus of (Co)Inductive
+ Constructions (CIC) implemented in the interactive theorem prover Matita. The
+ refinement algorithm is in charge of giving a meaning to the terms, types and
+ proof terms directly written by the user or generated by using tactics,
+ decision procedures or general automation. The terms are written in an
+ “external syntax” meant to be user friendly that allows omission of
+ information, untyped binders and a certain liberal use of user defined
+ sub-typing. The refiner modifies the terms to obtain related well typed terms
+ in the internal syntax understood by the kernel of the ITP. In particular, it
+ acts as a type inference algorithm when all the binders are untyped. The
+ proposed algorithm is bi-directional: given a term in external syntax and a
+ type expected for the term, it propagates as much typing information as
+ possible towards the leaves of the term. Traditional mono-directional
+ algorithms, instead, proceed in a bottom- up way by inferring the type of a
+ sub-term and comparing (unifying) it with the type expected by its context only
+ at the end. We propose some novel bi-directional rules for CIC that are
+ particularly effective. Among the benefits of bi-directionality we have better
+ error message reporting and better inference of dependent types. Moreover,
+ thanks to bi-directionality, the coercion system for sub-typing is more
+ effective and type inference generates simpler unification problems that are
+ more likely to be solved by the inherently incomplete higher order unification
+ algorithms implemented. Finally we introduce in the external syntax the notion
+ of vector of placeholders that enables to omit at once an arbitrary number of
+ arguments. Vectors of placeholders allow a trivial implementation of implicit
+ arguments and greatly simplify the implementation of primitive and simple
+ tactics.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ The Matita Interactive Theorem Prover
+ </span>
+ <a class="paper_download" href="PAPERS/system_description2011.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ In Automated Deduction – CADE-23, LECTURE NOTES IN COMPUTER SCIENCE,
+ ISBN:978-3-642-22437-9, Pages 64-69, Volume 6803, Year 2011 64-69.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Claudio Sacerdoti Coen, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ Nonuniform Coercions via Unification Hints
+ </span>
+ <a class="paper_download" href="PAPERS/nonunifcoerc.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ In Proceedings Types for Proofs and Programs, Revised Selected Papers,
+ ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE (EPTCS),
+ ISSN:2075-2180, DOI:10.4204/EPTCS.53.2, vol. 53, 19-26, March 2011.
+ </span>
+ <span class="paper_abstract">
+ We introduce the notion of nonuniform coercion, which is the promotion of a
+ value of one type to an enriched value of a different type via a nonuniform
+ procedure. Nonuniform coercions are a generalization of the (uniform) coercions
+ known in the literature and they arise naturally when formalizing mathematics in
+ an higher order interactive theorem prover using convenient devices like
+ canonical structures, type classes or unification hints. We also show how
+ nonuniform coercions can be naturally implemented at the user level in an
+ interactive theorem prover that allows unification hints.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ Hints in Unification
+ </span>
+ <a class="paper_download" href="PAPERS/tphol09.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ In Proceedings of Theorem Proving in Higher Order Logics (TPHOLs 2009),
+ Munich, August 17-20, 2009. LECTURE NOTES IN COMPUTER SCIENCE,
+ ISBN:978-3-642-03358-2, vol. 5674. 84-98.
+ </span>
+ <span class="paper_abstract">
+ Several mechanisms such as Canonical Structures, Type Classes, or
+ Pullbacks have been recently introduced with the aim to improve the power
+ and flexibility of the type inference algorithm for interactive theorem
+ provers. We claim that all these mechanisms are particular instances of a
+ simpler and more general technique, just consisting in providing suitable
+ hints to the unification procedure underlying type inference. This allows
+ a simple, modular and not intrusive implementation of all the above
+ mentioned techniques, opening at the same time innovative and unexpected
+ perspectives on its possible applications.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ Smart Matching
+ </span>
+ <a class="paper_download" href="PAPERS/smart.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Published in the proceedings of MKM2010, LNCS, Volume 6167/2010, Year 2010,
+ Pages 263-277, DOI 10.1007/978-3-642-14128-7_23, ISBN 978-3-642-14127-0.
+ </span>
+ <span class="paper_abstract">
+ One of the most annoying aspects in the formalization of
+ mathematics is the need of transforming notions to match a given, existing
+ result. This kind of transformations, often based on a conspicuous background
+ knowledge in the given scientific domain (mostly expressed in the form of
+ equalities or isomorphisms), are usually implicit in the mathematical
+ discourse, and it would be highly desirable to obtain a similar behavior in
+ interactive provers. The paper describes the superposition-based implementation
+ of this feature inside the Matita interactive theorem prover, focusing in
+ particular on the so called smart application tactic, supporting smart matching
+ between a goal and a given result.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ A New Type For Tactics
+ </span>
+ <a class="paper_download" href="PAPERS/plmms09.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ To appear in the proceedings of ACM SIGSAM PLMMS 2009, ISBN 978-1-60558-735-6.
+ Published as technical report UBLCS-2009-14.
+ </span>
+ <span class="paper_abstract">
+ The type of tactics in all (procedural) proof assistants is (a variant of)
+ the one introduced in LCF. We discuss why this is inconvenient and we
+ propose
+ a new type for tactics that 1) allows the implementation of more clever
+ tactics; 2) improves the implementation of declarative languages on top
+ of procedural ones; 3) allows for better proof structuring; 4) improves
+ proof automation; 5) allows tactics to rearrange and delay the goals to be
+ proved (e.g. in case of side conditions or PVS subtyping judgements).
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ A Compact Kernel for the Calculus of Inductive Constructions
+ </span>
+ <a class="paper_download" href="PAPERS/sadhana.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Published in the <a href="http://www.springer.com/engineering/journal/12046">Journal Sadhana</a>,
+ </span>
+ <span class="paper_abstract">
+ The paper describes the new kernel for the Calculus of Inductive
+ Constructions (CIC) implemented inside the Matita Interactive Theorem Prover.
+ The design of the new kernel has been completely revisited since
+ the first release, resulting in a remarkably compact implementation
+ of about 2300 lines of OCaml code. The work is meant for people
+ interested in implementation aspects of Interactive Provers, and
+ is not self contained. In particular, it requires good
+ acquaintance with Type Theory and functional programming languages.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ Higher order proof reconstruction from paramodulation-based refutations:
+ the unit equality case
+ </span>
+ <a class="paper_download" href="PAPERS/hopr.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2007: The 6th
+ International Conference on Mathematical Knowledge Management.
+ </span>
+ <span class="paper_abstract">
+ In this paper we address the problem of reconstructing a
+ higher order, checkable proof object starting from a proof trace left by a
+ first order automatic proof searching procedure, in a restricted equational
+ framework. The automatic procedure is based on superposition rules for
+ the unit equality case. Proof transformation techniques aimed to improve
+ the readability of the final proof are discussed.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Claudio Sacerdoti Coen, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Spurious Disambiguation Error Detection
+ </span>
+ <a class="paper_download" href="PAPERS/disambiguation-errors.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2007: The 6th
+ International Conference on Mathematical Knowledge Management.
+ </span>
+ <span class="paper_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 our
+ former efficient disambiguation algorithm.
+ </span>
+ </li>
<li class="paper">
<span class="paper_author">
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
</span><br/>
<span class="paper_title">
- The Matita Proof Assistant
+ Crafting a Proof Assistant
</span>
- <a class="paper_download" href="PAPERS/matita.pdf">
+ <a class="paper_download" href="PAPERS/matita_types.pdf">
<span class="pdf_logo">.pdf</span>
</a>
- <a class="paper_download" href="PAPERS/matita.ps">
- <span class="ps_logo">.ps</span>
- </a><br/>
<span class="paper_info">
- Submitted to Journal of Automated Reasoning, Special Issue on User
- Interfaces for Theorem Proving
+ Accepted for publication in the Proceedings of Types 2006: Conference of
+ the Types Project. Nottingham, UK -- April 18-21, 2006.
+ </span>
+ <span class="paper_abstract">
+ Proof assistants are complex applications whose develop-
+ ment has never been properly systematized or documented. This work is
+ a contribution in this direction, based on our experience with the devel-
+ opment 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 com-
+ parison between different systems and to highlight the common func-
+ tionalities, not only in view of reusability but also to encourage a more
+ systematic comparison of different softwares and architectural solutions.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
</span><br/>
+ <span class="paper_title">
+ User Interaction with the Matita Proof Assistant
+ </span>
+ <a class="paper_download" href="PAPERS/matita.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in Journal of Automated Reasoning, Special Issue
+ on User Interfaces for Theorem Proving.
+ </span>
<span class="paper_abstract">
- Matita is a new document-centric proof assistant that integrates several
- Mathematical Knowledge Management tools and techniques. In this paper we
- describe the architecture of Matita and the peculiarities of its user
- interface.
+ 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 search-
+ able knowledge base, the emphasis on a high-quality notational rendering, and the
+ complex interplay between syntax, presentation, and semantics.
</span>
</li>
<a class="paper_download" href="PAPERS/tinycals.pdf">
<span class="pdf_logo">.pdf</span>
</a>
- <a class="paper_download" href="PAPERS/tinycals.ps">
- <span class="ps_logo">.ps</span>
- </a><br/>
<span class="paper_info">
- Submitted to UITP 2006 User Interfaces for Theorem Provers. Seattle, WA
- -- August 21, 2006.
- </span><br/>
+ In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle,
+ WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 -
+ 142, ISSN:1571-0661
+ </span>
<span class="paper_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
<a class="paper_download" href="PAPERS/notation.pdf">
<span class="pdf_logo">.pdf</span>
</a>
- <a class="paper_download" href="PAPERS/notation.ps">
- <span class="ps_logo">.ps</span>
- </a><br/>
<span class="paper_info">
Accepted for publication in the proceedings of MKM 2006: The 5th
International Conference on Mathematical Knowledge Management.
Wokingham, UK -- August 11-12, 2006.
- </span><br/>
+ </span>
<span class="paper_abstract">
Mathematical notation is a structured, open, and ambiguous language. In
order to support mathematical notation in MKM applications one must
<a class="paper_download" href="PAPERS/whelp.pdf">
<span class="pdf_logo">.pdf</span>
</a>
- <a class="paper_download" href="PAPERS/whelp.ps">
- <span class="ps_logo">.ps</span>
- </a><br/>
<span class="paper_info">
In Proceedings of TYPES 2004 conference Types for Proofs and Programs.
Paris, France -- December 15-18, 2004. LNCS 3839/2004, Springer-Verlag
Heidelberg, ISBN 3-540-31428-8, pp. 17-32
- </span><br/>
+ </span>
<span class="paper_abstract">
The prototype of a content based search engine for mathematical knowledge
supporting a small set of queries requiring matching and/or typing
<a class="paper_download" href="PAPERS/disambiguation.pdf">
<span class="pdf_logo">.pdf</span>
</a>
- <a class="paper_download" href="PAPERS/disambiguation.ps">
- <span class="ps_logo">.ps</span>
- </a><br/>
<span class="paper_info">
In Proceedings of MKM 2004
Third International Conference on Mathematical Knowledge Management.
September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
- </span><br/>
+ </span>
<span class="paper_abstract">
Mathematical notation has the characteristic of being ambiguous:
operators can be overloaded and information that can be deduced is often
projects / helm.git / blobdiff