X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=c22db5e1ce9f03802dcbcb812811ff85175bef68;hb=2fbef023cc9fdb3d6982194ba62552a0605f2571;hp=6617949a5ebca6ca049d24e165402d2be6d403ca;hpb=e999e3e921dd6a7d2ef78e458bfbb26bdeaa4e7a;p=helm.git

diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index 6617949a5..c22db5e1c 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" -->
@@ -16,6 +16,53 @@
       Matita can be <a href="library/">browsed on line</a>.
       </p>
 
+      <br/>
+
+      <h1>Large Developments</h1>
+
+      <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; (lambda-delta)<a name="lambda-delta"></a></h2>
+      <p>
+      See the <a href="http://helm.cs.unibo.it/lambda-delta/">&lambda;&delta; home page</a>.
+      </p>
+
       <!--#include virtual="bottombar.shtml" -->
     </div>
   </body>
