X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=d065b7a9f643a104aac62d96577f14daf08ea5d7;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=a6f195b630f6c9f6eed33b9df899c8323de49fee;hpb=9d356a6f202a77fb1dd67b57b1c86ac3ebe1382b;p=helm.git

diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index a6f195b63..d065b7a9f 100644
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -1,6 +1,6 @@
-<!-- $Id$ -->
 <!--#include virtual="xhtml-header.shtml" -->
-<html>
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
   <head>
     <title>Matita - Library</title>
     <!--#include virtual="xhtml-meta.shtml" -->
@@ -12,14 +12,100 @@
 
       <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>
+      (Old <a href="library/">scripts</a> used in the previous releases of
+      Matita are <a href="library/">still available</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="http://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, funded 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 based on the minimalist type theory
+      by Maietti and Sambin, where choice axioms are not valid.
+      </p>
+      In order to reason comfortably 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 algebrized ones. In particular we formalized:
+      </p>
+      <ul>
+       <li>the large category of Overlap Algebras, that extends 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.
+           Morphisms of Overlap Algebras algebrize concrete relations between
+           sets by means of four functions that capture 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:
@@ -29,14 +115,14 @@
        <li>an executable formalization of the operational semantics of
            any <a href="http://www.freescale.com">Freescale</a>
            micro-controller of the <a href="http://www.freescale.com/webapp/sps/site/homepage.jsp?nodeId=0162468449&tid=FSH">HC05/HC08/RS08/HCS08 families</a>
+           </li>
        <li>a compiler from assembly language (pseudocodes + operands) to
-           machine code
+       machine code</li>
        <li>several automatic checks for unhandled opcodes, memory accesses,
-           correctness of ALU logic, etc.
+       correctness of ALU logic, etc.</li>
        <li>three examples of assembly programs (string reverse, counting sort
-           and perfect numbers sieve) with sets of data to run them
+       and perfect numbers sieve) with sets of data to run them</li>
       </ul>
-      </a>
       
       <p>The execution in the executable formalization has been compared
          to real world execution using the <a href="http://www.freescale.com/webapp/sps/site/overview.jsp?code=784_LPBBNEWTOOL&fsrch=1">USB SPYDER08</a>
@@ -58,6 +144,56 @@
          here</a>.
       </p>
 
+      <h2>The Formal System &lambda;&delta; (lambda_delta)<a name="lambda_delta"></a></h2>
+      
+      <p>The formal system &lambda;&delta; is a typed &lambda;-calculus that
+         pursues the unification of terms, types, environments and contexts
+	 as the main goal.
+         &lambda;&delta; takes some features from the Automath-related
+	 &lambda;-calculi and some from the pure type systems, but differs
+	 from both in that it does not include the &Pi; construction while it
+	 provides for an abbreviation mechanism at the level of terms.
+      </p>
+
+      <p> The development presents the proofs of some important properties that
+          &lambda;&delta; enjoys. In particular: 
+          <ul> <li> the confluence of reduction </li>
+               <li> the correctness of types </li>
+               <li> the uniqueness of types up to conversion </li>
+               <li> the subject reduction of the type assignment </li>
+               <li> the strong normalization of the typed terms </li>
+               <li> the decidability of type inference problem </li>
+          </ul>
+      </p>
+      
+      <p>
+       See the <a href="http://lambda-delta.info/">&lambda;&delta; home page</a>
+       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>
