+ <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 MKM07
+ </span><br/>
+ <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">
+ Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Crafting a Proof Assistant
+ </span>
+ <a class="paper_download" href="PAPERS/matita_types.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the Proceedings of Types 2006: Conference of
+ the Types Project. Nottingham, UK -- April 18-21, 2006.
+ </span><br/>
+ <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>
+
+