]> matita.cs.unibo.it Git - helm.git/blob - helm/www/matita/library.shtml
...
[helm.git] / helm / www / matita / 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
19       <br/>
20
21       <h1>Large Developments</h1>
22
23       <h2>Freescale<a name="freescale"></a></h2>
24       <p>
25       The <a href="freescale/">scripts</a> present:
26       </p>
27
28       <ul>
29        <li>an executable formalization of the operational semantics of
30            any <a href="http://www.freescale.com">Freescale</a>
31            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>
32            </li>
33        <li>a compiler from assembly language (pseudocodes + operands) to
34        machine code</li>
35        <li>several automatic checks for unhandled opcodes, memory accesses,
36        correctness of ALU logic, etc.</li>
37        <li>three examples of assembly programs (string reverse, counting sort
38        and perfect numbers sieve) with sets of data to run them</li>
39       </ul>
40       
41       <p>The execution in the executable formalization has been compared
42          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>
43         in-circuit debugger.
44       </p>
45
46       <p>
47        The code (in <a href="http://caml.inria.fr">OCaml</a>)
48        of an executable <a href="freescale/freescale_ocaml">emulator</a>,
49        automatically generated from the scripts above. On the tests above,
50        it runs at about 29% of the speed of the
51        <a href="http://www.freescale.com/codewarrior">CodeWarrior</a>
52        emulation engine.
53       </p>
54
55       <p>The formalization has been the Undergraduate Thesis of
56          Mr. Cosimo Oliboni. The manuscript (italian only) can be found
57          <a href="http://matita.cs.unibo.it/documentation.shtml#freescale">
58          here</a>.
59       </p>
60
61       <h2>The Formal System &lambda;&delta; (lambda-delta)<a name="lambda-delta"></a></h2>
62       
63       <p>The formal system &lambda;&delta; is a typed &lambda;-calculus that
64          pursues the unification of terms, types, environments and contexts
65          as the main goal.
66          &lambda;&delta; takes some features from the Automath-related
67          &lambda;-calculi and some from the pure type systems, but differs
68          from both in that it does not include the &Pi; construction while it
69          provides for an abbreviation mechanism at the level of terms.
70       </p>
71
72       <p> The development presents the proofs of some important properties that
73           &lambda;&delta; enjoys. In particular: 
74           <ul> <li> the confluence of reduction </li>
75                <li> the correctness of types </li>
76                <li> the uniqueness of types up to conversion </li>
77                <li> the subject reduction of the type assignment </li>
78                <li> the strong normalization of the typed terms </li>
79                <li> the decidability of type inference problem </li>
80           </ul>
81       </p>
82       
83       <p>
84        See the <a href="http://helm.cs.unibo.it/lambda-delta/">&lambda;&delta; home page</a>
85        for more information.
86       </p>
87
88       <!--#include virtual="bottombar.shtml" -->
89     </div>
90   </body>
91 </html>