From c2a490a6bc12986720b2c84d6916854c6931e08d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 13 Apr 2011 11:15:01 +0000
Subject: [PATCH] ...

---
 helm/www/matita/download.shtml |   2 +-
 helm/www/matita/library.shtml  | 106 +++++++++++++++++++++++++++++++++
 2 files changed, 107 insertions(+), 1 deletion(-)

diff --git a/helm/www/matita/download.shtml b/helm/www/matita/download.shtml
index bcafb843f..737ee6379 100644
--- a/helm/www/matita/download.shtml
+++ b/helm/www/matita/download.shtml
@@ -43,7 +43,7 @@
         <dt>Sources</dt>
         
         <dd>You can download the <a
-          href="FILES/matita_0.5.8.orig.tar.gz">sources</a> of Matita (around 6 MB, md5sum:
+          href="FILES/matita-0.5.8.orig.tar.gz">sources</a> of Matita (around 6 MB, md5sum:
 125223d3dc522c4ac063a66f5d46df69 
         )
         and
diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index 3c4246f31..9874142c9 100644
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -15,11 +15,94 @@
       The <a href="library/">scripts</a> used to generate the knowledge base of
       Matita can be <a href="library/">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>.
+      </p>
 
       <br/>
 
       <h1>Large Developments</h1>
 
+      <h2>Certified Complexity (CerCo)<a name="cerco"></a></h2>
+      <p>Matita is being used to certify a cost preserving compiler from a
+         large subset of C into the 8051 machine code. The compiler does not
+         only produce the target code, but it also instruments the source code
+         with precise cost declarations for the execution of O(1) code
+         fragments. This induced cost model for the source language is
+         inherently non compositional since it is affected by the compilation
+         strategy: the same instructions are compiled in different ways in
+         different contexts, yielding different costs.
+       </p>
+       <p>The final aim of the CerCo project is to formally reason on
+         intensional properties on the C code -- e.g. to show that some hard
+         deadline is always met
+         -- and to be sure that the property holds also for the target code.
+       </p>
+       <p>The CerCo project is a FET Open IST project funded by the EU
+          community in the 7th Framework Programme. More informations on the
+          project and the code of the Matita formalization can be found
+          on the <a href="cerco.cs.unibo.it">CerCo Web site</a>
+       </p>
+
+      <h2>The Basic Picture<a name="sambin"></a></h2>
+      <p>
+      The <a href="library/formal_topology">scripts</a> present a formalization
+      of some results from the forthcoming book <a href="http://www.oup.com/us/catalog/general/subject/Mathematics/Logic/?view=usa&ci=9780199232888">The Basic Picture - Structures for Constructive Topology</a> by Giovanni Sambin.
+      </p>
+      <p>The formalization has been the result of a three years long
+       collaboration between mathematicians from the University of Padova
+       and computer scientists from the University of
+       Bologna, sponsored by the University of Padova. In particular,
+       the groups that collaborated are headed respectively by Prof. Sambin
+       in Padua (formal topology and constructive type theory)
+       and by Prof. Asperti in Bologna (constructive type theory and interactive
+       theorem proving).
+      </p>
+      <p>
+      In particular the <a href="library/formal_topology">scripts</a> present:
+      </p>
+      <ul>
+       <li>the category of Basic Pairs, that are generalizations of
+           topological spaces</li>
+       <li>the category of Basic Topologies, that are generalizations of
+           formal topologies</li>
+       <li>the existence of a categorical embedding of the former category
+           into the latter. The embedding is an improvement on the usual
+           adjunction between topological spaces and locales</li>
+      </ul>
+      <p>
+      All the results are presented constructively and in the predicative
+      fragment of Matita, without any reference to choice axioms.
+      </p>
+      In order to reason conformtably on the previous concrete categories and
+      functors, we also present algebraic versions of all the introduced
+      notions, as well as categorical embedding of the concrete categories in
+      the algebraized ones. In particular we formalized:
+      </p>
+      <ul>
+       <li>the large category of Overlap Algebras, that extend locales with an
+           axiomatized (= algebraized) overlap binary predicate. The
+           concrete overlap predicate states positively 
+           (i.e. without using negation) the existence (in the intuitionistic
+           sense) of a point in the intersection of two sets.
+           The natural morphism over Overlap Algebras are functions for the
+           existential and universal pre and post images of a relation.
+           </li>
+       <li>the large category of O-Basic Pairs, that algebraize Basic
+           Pairs by means of Overlap Algebras</li>
+       <li>the large category of O-Basic Topologies, that algebraize Basic
+           Topologies by means of Overlap Algebras</li>
+       <li>the categorical embedding of Basic Pairs into O-Basic Pairs and
+           of Basic Topologies into O-Basic Topologies</li>
+       <li>the existence of a categorical embedding of the category
+           of O-Basic Pairs into the category of O-Basic Topologies</li>
+      </ul>
+      <p>
+      More information will be available in a forthcoming paper by
+      Claudio Sacerdoti Coen and Enrico Tassi to be
+      published in the Mathematical Structures in Computer Science journal.
+      </p>
+
       <h2>Freescale<a name="freescale"></a></h2>
       <p>
       The <a href="freescale/">scripts</a> present:
@@ -85,6 +168,29 @@
        for more information.
       </p>
 
+      <h1>Small Developments</h1>
+
+      <h2>Pointed regular expressions<a name="freescale"></a></h2>
+      <p>
+      The <a href="re/">script</a> present:
+      </p>
+
+      <ul>
+       <li>a formalization of the syntax and semantics of pointed regular
+           expressions, that are regular expressions where points are put
+           in front of atoms to describe where the next character recognized
+           by the expression should be. Multiple points represent the union
+           of multiple languages. A pointed regular expression corresponds
+           to a state of a regular automaton for the regular expression
+           obtained erasing all points.</li>
+       <li>a formalization of the construction of the automaton for a regular
+           expression by means of iterative computation of pointed regular
+           expressions.</li>
+       <li>a proof of correctness of the construction (to be completed)</li>
+      </ul>
+
+      <p>The development requires the SVN version of Matita to be executed.</p>
+
       <!--#include virtual="bottombar.shtml" -->
     </div>
   </body>
-- 
2.39.2