X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fpapers.shtml;h=6425ca683752cdb6db45f8f611e3f77349f2f9aa;hb=258d2e384e8bf7008d2fb01c7d3fee5126d65120;hp=886a87271e47a734652882b4e974812ab41fe16c;hpb=9d356a6f202a77fb1dd67b57b1c86ac3ebe1382b;p=helm.git

diff --git a/helm/www/matita/papers.shtml b/helm/www/matita/papers.shtml
index 886a87271..6425ca683 100644
--- a/helm/www/matita/papers.shtml
+++ b/helm/www/matita/papers.shtml
@@ -3,6 +3,198 @@
 </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">