-<!-- $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" -->
<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="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:
+ </p>
+
+ <ul>
+ <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</li>
+ <li>several automatic checks for unhandled opcodes, memory accesses,
+ 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</li>
+ </ul>
+
+ <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>
+ in-circuit debugger.
+ </p>
+
+ <p>
+ The code (in <a href="http://caml.inria.fr">OCaml</a>)
+ of an executable <a href="freescale/freescale_ocaml">emulator</a>,
+ automatically generated from the scripts above. On the tests above,
+ it runs at about 29% of the speed of the
+ <a href="http://www.freescale.com/codewarrior">CodeWarrior</a>
+ emulation engine.
+ </p>
+
+ <p>The formalization has been the Undergraduate Thesis of
+ Mr. Cosimo Oliboni. The manuscript (italian only) can be found
+ <a href="http://matita.cs.unibo.it/documentation.shtml#freescale">
+ here</a>.
+ </p>
+
+ <h2>The Formal System λδ (lambda_delta)<a name="lambda_delta"></a></h2>
+
+ <p>The formal system λδ is a typed λ-calculus that
+ pursues the unification of terms, types, environments and contexts
+ as the main goal.
+ λδ takes some features from the Automath-related
+ λ-calculi and some from the pure type systems, but differs
+ from both in that it does not include the Π 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
+ λδ 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/">λδ 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>