2 <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
7 <span class="paper_author">
8 Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
10 <span class="paper_title">
11 A Bi-directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
13 <a class="paper_download" href="PAPERS/lmcs_types_2010.pdf">
14 <span class="pdf_logo">.pdf</span>
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.
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
50 <span class="paper_author">
51 Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
53 <span class="paper_title">
54 The Matita Interactive Theorem Prover
56 <a class="paper_download" href="PAPERS/system_description2011.pdf">
57 <span class="pdf_logo">.pdf</span>
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.
66 <span class="paper_author">
67 Claudio Sacerdoti Coen, Enrico Tassi
69 <span class="paper_title">
70 Nonuniform Coercions via Unification Hints
72 <a class="paper_download" href="PAPERS/nonunifcoerc.pdf">
73 <span class="pdf_logo">.pdf</span>
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.
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.
93 <span class="paper_author">
94 Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
96 <span class="paper_title">
99 <a class="paper_download" href="PAPERS/tphol09.pdf">
100 <span class="pdf_logo">.pdf</span>
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.
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.
121 <span class="paper_author">
122 Andrea Asperti, Enrico Tassi
124 <span class="paper_title">
127 <a class="paper_download" href="PAPERS/smart.pdf">
128 <span class="pdf_logo">.pdf</span>
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.
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.
149 <span class="paper_author">
150 Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
152 <span class="paper_title">
153 A New Type For Tactics
155 <a class="paper_download" href="PAPERS/plmms09.pdf">
156 <span class="pdf_logo">.pdf</span>
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.
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
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).
175 <span class="paper_author">
176 Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
178 <span class="paper_title">
179 A Compact Kernel for the Calculus of Inductive Constructions
181 <a class="paper_download" href="PAPERS/sadhana.pdf">
182 <span class="pdf_logo">.pdf</span>
184 <span class="paper_info">
185 Published in the <a href="http://www.springer.com/engineering/journal/12046">Journal Sadhana</a>,
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.
200 <span class="paper_author">
201 Andrea Asperti, Enrico Tassi
203 <span class="paper_title">
204 Higher order proof reconstruction from paramodulation-based refutations:
205 the unit equality case
207 <a class="paper_download" href="PAPERS/hopr.pdf">
208 <span class="pdf_logo">.pdf</span>
210 <span class="paper_info">
211 Accepted for publication in the proceedings of MKM 2007: The 6th
212 International Conference on Mathematical Knowledge Management.
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.
225 <span class="paper_author">
226 Claudio Sacerdoti Coen, Stefano Zacchiroli
228 <span class="paper_title">
229 Spurious Disambiguation Error Detection
231 <a class="paper_download" href="PAPERS/disambiguation-errors.pdf">
232 <span class="pdf_logo">.pdf</span>
234 <span class="paper_info">
235 Accepted for publication in the proceedings of MKM 2007: The 6th
236 International Conference on Mathematical Knowledge Management.
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.
250 <span class="paper_author">
251 Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
253 <span class="paper_title">
254 Crafting a Proof Assistant
256 <a class="paper_download" href="PAPERS/matita_types.pdf">
257 <span class="pdf_logo">.pdf</span>
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.
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.
280 <span class="paper_author">
281 Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
283 <span class="paper_title">
284 User Interaction with the Matita Proof Assistant
286 <a class="paper_download" href="PAPERS/matita.pdf">
287 <span class="pdf_logo">.pdf</span>
289 <span class="paper_info">
290 Accepted for publication in Journal of Automated Reasoning, Special Issue
291 on User Interfaces for Theorem Proving.
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.
304 <span class="paper_author">
305 Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
307 <span class="paper_title">
308 Tinycals: step by step tacticals
310 <a class="paper_download" href="PAPERS/tinycals.pdf">
311 <span class="pdf_logo">.pdf</span>
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 -
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
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.
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
341 <a class="paper_download" href="PAPERS/notation.pdf">
342 <span class="pdf_logo">.pdf</span>
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.
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.
366 <span class="paper_author">
367 Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
369 <span class="paper_title">
370 A content based mathematical search engine: Whelp
372 <a class="paper_download" href="PAPERS/whelp.pdf">
373 <span class="pdf_logo">.pdf</span>
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
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.
394 <span class="paper_author">
395 Claudio Sacerdoti Coen, Stefano Zacchiroli
397 <span class="paper_title">
398 Efficient Ambiguous Parsing of Mathematical Formulae
400 <a class="paper_download" href="PAPERS/disambiguation.pdf">
401 <span class="pdf_logo">.pdf</span>
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
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.
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.
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.