1 <!--#include virtual="xhtml-header.shtml" -->
3 <html xmlns="http://www.w3.org/1999/xhtml">
5 <title>Matita - Library</title>
6 <!--#include virtual="xhtml-meta.shtml" -->
9 <!--#include virtual="menubar.shtml" -->
11 <h1>Matita Library</h1>
13 <h2>Scripts<a name="scripts"></a></h2>
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>.
21 <h1>Large Developments</h1>
23 <h2>Freescale<a name="freescale"></a></h2>
25 The <a href="freescale/">scripts</a> present:
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>
33 <li>a compiler from assembly language (pseudocodes + operands) to
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>
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>
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>
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">
61 <h2>The Formal System λδ (lambda-delta)<a name="lambda-delta"></a></h2>
63 See the <a href="http://helm.cs.unibo.it/lambda-delta/">λδ home page</a>.
66 <!--#include virtual="bottombar.shtml" -->