-<!-- $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" -->
<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
+ machine code</li>
<li>several automatic checks for unhandled opcodes, memory accesses,
- correctness of ALU logic, etc.
+ 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
+ and perfect numbers sieve) with sets of data to run them</li>
</ul>
- </a>
<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>
here</a>.
</p>
+ <h2>The Formal System λδ (lambda-delta)<a name="lambda-delta"></a></h2>
+ <p>
+ See the <a href="http://helm.cs.unibo.it/lambda-delta/">λδ home page</a>.
+ </p>
+
<!--#include virtual="bottombar.shtml" -->
</div>
</body>
projects / helm.git / blobdiff