helm/www/matita1.0/library.shtml

   1 <!--#include virtual="xhtml-header.shtml" -->
   2 <!-- $Id$ -->
   3 <html xmlns="http://www.w3.org/1999/xhtml">
   4   <head>
   5     <title>Matita - Library</title>
   6     <!--#include virtual="xhtml-meta.shtml" -->
   7   </head>
   8   <body>
   9     <!--#include virtual="menubar.shtml" -->
  10     <div class="main">
  11       <h1>Matita Library</h1>
  12
  13       <h2>Scripts<a name="scripts"></a></h2>
  14       <p>
  15       The <a href="library/">scripts</a> used to generate the knowledge base of
  16       Matita can be <a href="library/">browsed on line</a>.
  17       </p>
  18       <p>
  19       The experimental <a href="nlibrary/">scripts</a> for the next major version of Matita can also be <a href="nlibrary/">browsed on line</a>.
  20       </p>
  21
  22       <br/>
  23
  24       <h1>Large Developments</h1>
  25
  26       <h2>Certified Complexity (CerCo)<a name="cerco"></a></h2>
  27       <p>Matita is being used to certify a cost preserving compiler from a
  28          large subset of C into the 8051 machine code. The compiler does not
  29          only produce the target code, but it also instruments the source code
  30          with precise cost declarations for the execution of O(1) code
  31          fragments. This induced cost model for the source language is
  32          inherently non compositional since it is affected by the compilation
  33          strategy: the same instructions are compiled in different ways in
  34          different contexts, yielding different costs.
  35        </p>
  36        <p>The final aim of the CerCo project is to formally reason on
  37          intensional properties on the C code -- e.g. to show that some hard
  38          deadline is always met
  39          -- and to be sure that the property holds also for the target code.
  40        </p>
  41        <p>The CerCo project is a FET Open IST project funded by the EU
  42           community in the 7th Framework Programme. More informations on the
  43           project and the code of the Matita formalization can be found
  44           on the <a href="cerco.cs.unibo.it">CerCo Web site</a>
  45        </p>
  46
  47       <h2>The Basic Picture<a name="sambin"></a></h2>
  48       <p>
  49       The <a href="library/formal_topology">scripts</a> present a formalization
  50       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.
  51       </p>
  52       <p>The formalization has been the result of a three years long
  53        collaboration between mathematicians from the University of Padova
  54        and computer scientists from the University of
  55        Bologna, funded by the University of Padova. In particular,
  56        the groups that collaborated are headed respectively by Prof. Sambin
  57        in Padua (formal topology and constructive type theory)
  58        and by Prof. Asperti in Bologna (constructive type theory and interactive
  59        theorem proving).
  60       </p>
  61       <p>
  62       In particular the <a href="library/formal_topology">scripts</a> present:
  63       </p>
  64       <ul>
  65        <li>the category of Basic Pairs, that are generalizations of
  66            topological spaces</li>
  67        <li>the category of Basic Topologies, that are generalizations of
  68            formal topologies</li>
  69        <li>the existence of a categorical embedding of the former category
  70            into the latter. The embedding is an improvement on the usual
  71            adjunction between topological spaces and locales</li>
  72       </ul>
  73       <p>
  74       All the results are presented constructively and in the predicative
  75       fragment of Matita based on the minimalist type theory
  76       by Maietti and Sambin, where choice axioms are not valid.
  77       </p>
  78       In order to reason comfortably on the previous concrete categories and
  79       functors, we also present algebraic versions of all the introduced
  80       notions, as well as categorical embedding of the concrete categories in
  81       the algebrized ones. In particular we formalized:
  82       </p>
  83       <ul>
  84        <li>the large category of Overlap Algebras, that extends locales with an
  85            axiomatized (= algebraized) overlap binary predicate. The
  86            concrete overlap predicate states positively
  87            (i.e. without using negation) the existence (in the intuitionistic
  88            sense) of a point in the intersection of two sets.
  89            Morphisms of Overlap Algebras algebrize concrete relations between
  90            sets by means of four functions that capture the
  91            existential and universal pre and post images of a relation.
  92            </li>
  93        <li>the large category of O-Basic Pairs, that algebraize Basic
  94            Pairs by means of Overlap Algebras</li>
  95        <li>the large category of O-Basic Topologies, that algebraize Basic
  96            Topologies by means of Overlap Algebras</li>
  97        <li>the categorical embedding of Basic Pairs into O-Basic Pairs and
  98            of Basic Topologies into O-Basic Topologies</li>
  99        <li>the existence of a categorical embedding of the category
 100            of O-Basic Pairs into the category of O-Basic Topologies</li>
 101       </ul>
 102       <p>
 103       More information will be available in a forthcoming paper by
 104       Claudio Sacerdoti Coen and Enrico Tassi to be
 105       published in the Mathematical Structures in Computer Science journal.
 106       </p>
 107
 108       <h2>Freescale<a name="freescale"></a></h2>
 109       <p>
 110       The <a href="freescale/">scripts</a> present:
 111       </p>
 112
 113       <ul>
 114        <li>an executable formalization of the operational semantics of
 115            any <a href="http://www.freescale.com">Freescale</a>
 116            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>
 117            </li>
 118        <li>a compiler from assembly language (pseudocodes + operands) to
 119        machine code</li>
 120        <li>several automatic checks for unhandled opcodes, memory accesses,
 121        correctness of ALU logic, etc.</li>
 122        <li>three examples of assembly programs (string reverse, counting sort
 123        and perfect numbers sieve) with sets of data to run them</li>
 124       </ul>
 125
 126       <p>The execution in the executable formalization has been compared
 127          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>
 128         in-circuit debugger.
 129       </p>
 130
 131       <p>
 132        The code (in <a href="http://caml.inria.fr">OCaml</a>)
 133        of an executable <a href="freescale/freescale_ocaml">emulator</a>,
 134        automatically generated from the scripts above. On the tests above,
 135        it runs at about 29% of the speed of the
 136        <a href="http://www.freescale.com/codewarrior">CodeWarrior</a>
 137        emulation engine.
 138       </p>
 139
 140       <p>The formalization has been the Undergraduate Thesis of
 141          Mr. Cosimo Oliboni. The manuscript (italian only) can be found
 142          <a href="http://matita.cs.unibo.it/documentation.shtml#freescale">
 143          here</a>.
 144       </p>
 145
 146       <h2>The Formal System &lambda;&delta; (lambda_delta)<a name="lambda_delta"></a></h2>
 147
 148       <p>The formal system &lambda;&delta; is a typed &lambda;-calculus that
 149          pursues the unification of terms, types, environments and contexts
 150          as the main goal.
 151          &lambda;&delta; takes some features from the Automath-related
 152          &lambda;-calculi and some from the pure type systems, but differs
 153          from both in that it does not include the &Pi; construction while it
 154          provides for an abbreviation mechanism at the level of terms.
 155       </p>
 156
 157       <p> The development presents the proofs of some important properties that
 158           &lambda;&delta; enjoys. In particular:
 159           <ul> <li> the confluence of reduction </li>
 160                <li> the correctness of types </li>
 161                <li> the uniqueness of types up to conversion </li>
 162                <li> the subject reduction of the type assignment </li>
 163                <li> the strong normalization of the typed terms </li>
 164                <li> the decidability of type inference problem </li>
 165           </ul>
 166       </p>
 167
 168       <p>
 169        See the <a href="http://lambda-delta.info/">&lambda;&delta; home page</a>
 170        for more information.
 171       </p>
 172
 173       <h1>Small Developments</h1>
 174
 175       <h2>Pointed regular expressions<a name="freescale"></a></h2>
 176       <p>
 177       The <a href="re/">script</a> present:
 178       </p>
 179
 180       <ul>
 181        <li>a formalization of the syntax and semantics of pointed regular
 182            expressions, that are regular expressions where points are put
 183            in front of atoms to describe where the next character recognized
 184            by the expression should be. Multiple points represent the union
 185            of multiple languages. A pointed regular expression corresponds
 186            to a state of a regular automaton for the regular expression
 187            obtained erasing all points.</li>
 188        <li>a formalization of the construction of the automaton for a regular
 189            expression by means of iterative computation of pointed regular
 190            expressions.</li>
 191        <li>a proof of correctness of the construction (to be completed)</li>
 192       </ul>
 193
 194       <p>The development requires the SVN version of Matita to be executed.</p>
 195
 196       <!--#include virtual="bottombar.shtml" -->
 197     </div>
 198   </body>
 199 </html>