From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Tue, 3 Apr 2012 11:31:03 +0000 (+0000)
Subject: Various updates to the (obsolete) website.
X-Git-Tag: make_still_working~1823
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c6ebbcf8350dcf0b8020c9fcea27d7d9336df463;p=helm.git

Various updates to the (obsolete) website.
---

diff --git a/helm/www/matita/development.shtml b/helm/www/matita/development.shtml
index 369176395..dae6c19d4 100644
--- a/helm/www/matita/development.shtml
+++ b/helm/www/matita/development.shtml
@@ -23,7 +23,7 @@
       <ul class="wide">
 	<li><a href="http://www.cs.unibo.it/~asperti/">Andrea Asperti</a> - Full Professor</li>
 	<li><a href="http://www.cs.unibo.it/~fguidi/">Ferruccio Guidi</a> - PhD</li>
-	<li><a href="http://ricciott.web.cs.unibo.it/">Wilmer Ricciotti</a> - PhD Student </li>
+	<li><a href="http://www.cs.unibo.it/~ricciott/">Wilmer Ricciotti</a> - PhD </li>
 	<li><a href="http://www.cs.unibo.it/~sacerdot/">Claudio Sacerdoti Coen</a> - Lecturer </li>
 	<li><a href="http://www.cs.unibo.it/~tassi/">Enrico Tassi</a> - PhD </li>
       </ul>
diff --git a/helm/www/matita/documentation.shtml b/helm/www/matita/documentation.shtml
index 66aab892c..ed0a51ed8 100644
--- a/helm/www/matita/documentation.shtml
+++ b/helm/www/matita/documentation.shtml
@@ -46,7 +46,10 @@
       <p> The source code of the user manual (in <a
 	href="http://www.oasis-open.org/docbook/">DocBook</a> format) is
       available from our repository, in the
-      <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fhelm%2Fsoftware%2Fmatita%2Fhelp%2FC%2F&amp;rev=0&amp;sc=0">matita/help/C/</a> folder. </p>
+      <a
+	href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fmatita%2Fmatita%2Fhelp%2FC%2F&#a984ecdd087e75087ba2f4b21276224c4">matita/help/C/</a> folder. </p>
+
+<!-- XXX: OUTDATED (WR)
 
       <h2>Tutorials<a name="tutorial"></a></h2>
 
@@ -71,14 +74,18 @@
       <a href="http://typessummerschool07.cs.unibo.it">types summer school 2007</a>
       by C.Sacerdoti and E.Tassi.
       </p>
+      -->
 
       <h2>Publications</h2>
       <!--#include virtual="papers.shtml" -->
 
+      <!-- XXX: OUTDATED (WR)
       <h2>Large Developments</h2>
-      <!--#include virtual="theses.shtml" -->
+      include virtual="theses.shtml"
+      -->
 
       <!--#include virtual="bottombar.shtml" -->
     </div>
   </body>
+
 </html>
diff --git a/helm/www/matita/download.shtml b/helm/www/matita/download.shtml
index 737ee6379..f6b7984b6 100644
--- a/helm/www/matita/download.shtml
+++ b/helm/www/matita/download.shtml
@@ -10,9 +10,43 @@
     <div class="main">
       <h1>Download Matita!</h1>
 
-      <h2>Releases<a name="releases"></a></h2>
+      <h2>Release<a name="testingreleases"></a></h2>
       <p>
-      The current version is 0.5.8, released on January 8, 2010. Here the 
+      The most recent version of Matita (0.99.1) is available as a LiveCD, or by
+      downloading the source code.
+      </p>
+      <dl>
+        <dt>Live DVD</dt>
+
+        <!--
+        <dd>Coming soon</dd>
+        -->
+        <dd>The <a href="FILES/matita-0.99.1.iso">live DVD</a> (around 900
+        MB, md5sum: 1f3af2eb8952fe19853bad88816cdff5) 
+        is the easiest way to try Matita. You can burn the ISO image to a DVD
+        and boot you computer from it, or install a free emulator like <a
+          href="http://virtualbox.org">virtualbox</a> and boot a virtual
+        machine from the ISO image. Virtualbox is available for Mac OS X,
+        Windows and Linux. A short guide to VirtualBox is part of the 
+        <a href="docs/manual/html">Matita manual</a><br/>
+        </dd>
+
+        <dt>Sources</dt>
+        
+        <dd>You can download the <a
+	  href="sources/matita_130312.tar.gz">sources</a> of Matita (released on
+	March 13th, 2012; around
+	10 MB, md5sum: 2ac55c06dd789fd38c13a0e0cc10bb3c)
+        and
+        build it by yourself, following the <a
+          href="docs/manual/html/sec_install.html">installation instructions</a>.
+        The build process, due to the high number of external dependency is not
+	trivial, we thus suggest that you try the live DVD instead.</dd> 
+      </dl>
+
+      <h2>Old releases (unsupported)<a name="releases"></a></h2>
+      <p>
+      Version is 0.5.8, released on January 8, 2010. Here the 
       <a href="http://helm.cs.unibo.it/websvn/filedetails.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fmatita%2Fdist%2FChangeLog&rev=0&sc=0">ChangeLog</a>.
       </p>
       <dl>
@@ -67,6 +101,7 @@
       You can <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2F&amp;sc=0">browse our svn repository</a> directly on the web.
       </p>
 
+      <!--
       <h2>Nightly builds<a name="nightly"></a></h2>
       <p>
       A build of the Debian package is performed every night, and a live CD containing that version is also built.
@@ -77,6 +112,7 @@
       deb http://matita.cs.unibo.it/DEBIAN ./
       deb-src http://matita.cs.unibo.it/DEBIAN ./
       </pre>
+      -->
       
       <h2>Cluster .cs.unibo.it.<a name="clustercs"></a></h2>
       <p>
diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index c42fa673b..e5aa7316e 100644
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -12,11 +12,12 @@
 
       <h2>Scripts<a name="scripts"></a></h2>
       <p>
-      The <a href="library/">scripts</a> used to generate the knowledge base of
-      Matita can be <a href="library/">browsed on line</a>.
+      The <a href="nlibrary/">scripts</a> used to generate the knowledge base of
+      Matita can be <a href="nlibrary/">browsed on line</a>.
       </p>
       <p>
-      The experimental <a href="nlibrary/">scripts</a> for the next major version of Matita can also be <a href="nlibrary/">browsed on line</a>.
+      (Old <a href="library/">scripts</a> used in the previous releases of
+      Matita are <a href="library/">still available</a>.)
       </p>
 
       <br/>
diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 0a331f58b..05ed186c0 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -58,6 +58,7 @@
       assembly of the kind traditionally used in embedded systems.
       </p>
       
+      <!--#include virtual="bottombar.shtml" -->
 
     </div>
   </body>
diff --git a/helm/www/matita/matita_it.shtml b/helm/www/matita/matita_it.shtml
index 8235b013a..0d77ec373 100644
--- a/helm/www/matita/matita_it.shtml
+++ b/helm/www/matita/matita_it.shtml
@@ -57,6 +57,8 @@
       da linguaggio C verso un linguaggio assembly tipico di microprocessori
       per sistemi embedded.</p>
 
+      <!--#include virtual="bottombar.shtml" -->
+
     </div>
   </body>
 </html>
diff --git a/helm/www/matita/matitaweb.shtml b/helm/www/matita/matitaweb.shtml
new file mode 100644
index 000000000..f2a605798
--- /dev/null
+++ b/helm/www/matita/matitaweb.shtml
@@ -0,0 +1,46 @@
+<!--#include virtual="xhtml-header.shtml" -->
+<!-- $Id: documentation.shtml 10623 2010-01-07 22:53:47Z tassi $ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
+  <head>
+    <title>Matita - Documentation</title>
+    <!--#include virtual="xhtml-meta.shtml" -->
+<script type="text/javascript">
+  function toggleAbstracts() {
+    abstracts = document.getElementsByTagName("span");
+    len = abstracts.length;
+    for (i=0; i != len-1; i++) {
+      elt = abstracts.item(i);
+      if (elt.hasAttribute("class")) {
+	if (elt.getAttribute("class") == "paper_abstract") {
+	  if (elt.style.display != "none") {
+	    elt.style.display = "none";
+	  } else {
+	    elt.style.display = "inline";
+	  }
+	}
+      }
+    }
+  }
+</script>
+  </head>
+  <body>
+    <!--#include virtual="menubar.shtml" -->
+    <div class="main">
+      <h1>Matita Web application</h1>
+
+      <p>Matita is available as a multi-user web application running remotely
+      on our server.</p>
+
+      <p><a href="http://pandemia.helm.cs.unibo.it/register.html">Register</a> now
+      to gain access to Matitaweb.</p>
+      
+      <p>If you already have a Matitaweb account, <a
+	href="http://pandemia.helm.cs.unibo.it/login.html">Click here</a> to log
+      in.</p>
+
+    <!--#include virtual="bottombar.shtml" -->
+
+    </div>
+  </body>
+
+</html>
diff --git a/helm/www/matita/menubar.shtml b/helm/www/matita/menubar.shtml
index 3c06e1836..81d3c744f 100644
--- a/helm/www/matita/menubar.shtml
+++ b/helm/www/matita/menubar.shtml
@@ -15,6 +15,7 @@
     </li>
     <li> <a href="development.shtml">Developers</a> </li>
     <li> <a href="community.shtml">Community</a> </li>
+    <li> <a href="matitaweb.shtml">Matitaweb</a> </li>
     <li> <a href="download.shtml">Download</a> </li>
   </ul>
 </div>
diff --git a/helm/www/matita/news.shtml b/helm/www/matita/news.shtml
index 7c448cf6c..d0646f66f 100644
--- a/helm/www/matita/news.shtml
+++ b/helm/www/matita/news.shtml
@@ -3,6 +3,17 @@
 <div class="news">
   <div class="newsheader">News</div>
   <ul class="news">
+    <li><span class="date">13 March 2012</span><br />
+    The <a href="matitaweb.shtml">Matita web app</a> is now publicly accessible
+    online (<a href="http://pandemia.helm.cs.unibo.it/">go</a>).
+    </li>
+    <li><span class="date">13 March 2012</span><br />
+    Matita release 0.99.1 available for <a href="download.shtml">download</a>.
+    </li>
+    <li><span class="date">1 February 2010</span><br />
+    Project <a href="http://cerco.cs.unibo.it/">CerCo</a> (Certified
+    Complexity) started.
+    </li>
     <li><span class="date">8 January 2010</span><br />
     Matita release 0.5.8 available for <a href="download.shtml">download</a>.
     </li>
@@ -30,6 +41,7 @@
     <li><span class="date">10 May 2008</span><br />
     Matita release 0.5.0 available for <a href="download.shtml">download</a>.
     </li>
+    <!--
     <li><span class="date">18 Dec 2007</span><br />
     Matita release candidate 0.4.98 available for <a href="download.shtml">download</a>.
     </li>
@@ -60,6 +72,7 @@
     <a href="community.shtml#lists">mailing lists</a> for Matita are now
     available
     </li>
+    -->
   </ul>
 </div>
 
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">