From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 10 May 2008 10:14:42 +0000 (+0000)
Subject: some files orphaned
X-Git-Tag: make_still_working~5241
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5182c0d2626f78e30da512c52aad59d7021b960a;p=helm.git

some files orphaned
---

diff --git a/helm/www/matita/PAPERS/oliboni.pdf b/helm/www/matita/PAPERS/oliboni.pdf
new file mode 100644
index 000000000..c65f859e5
Binary files /dev/null and b/helm/www/matita/PAPERS/oliboni.pdf differ
diff --git a/helm/www/matita/sources/matita-0.1.0.tar.gz b/helm/www/matita/sources/matita-0.1.0.tar.gz
deleted file mode 100644
index 6ab225f06..000000000
Binary files a/helm/www/matita/sources/matita-0.1.0.tar.gz and /dev/null differ
diff --git a/helm/www/matita/sources/matita-latest.tar.gz b/helm/www/matita/sources/matita-latest.tar.gz
deleted file mode 120000
index 851a6477c..000000000
--- a/helm/www/matita/sources/matita-latest.tar.gz
+++ /dev/null
@@ -1 +0,0 @@
-matita-0.1.0.tar.gz
\ No newline at end of file
diff --git a/helm/www/matita/theses.shtml b/helm/www/matita/theses.shtml
new file mode 100644
index 000000000..37a2b4117
--- /dev/null
+++ b/helm/www/matita/theses.shtml
@@ -0,0 +1,39 @@
+<!--
+<small>
+  <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
+</small>
+-->
+
+<ul>
+  
+  <li class="paper">
+  <a name="freescale"/>
+  <span class="paper_author">
+    Cosimo Arndt Oliboni
+  </span><br/>
+  <span class="paper_title">
+    Matita come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva
+    dei Microcontroller a 8 bit Freescale
+  </span>
+  <a class="paper_download" href="PAPERS/oliboni.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <span class="paper_info">
+    Undergraduate thesis, University of Bologna, 2008.
+  </span>
+  <span class="XXXpaper_abstract">
+   We describe an executable formalization of the operational semantics of
+   every microcontroller of the Freescale 8-bit families (HC05, HC08, HCS08,
+   RS08). The formalization is done in Matita and heavily relies on dependent
+   types (for static checking) and executable exhaustive tests (to avoid
+   under-specification and specification errors). Real world programs have
+   been compiled to assembly (using CodeWarrior) and executed both with
+   the emulator formalized in Matita and its extracted OCaml version (for
+   performance reasons). All aspects of memory management and execution are
+   captured, up to the point of precisely characterizing the number of clock
+   cycles required by any single instruction. The manuscript is in Italian
+   only.
+  </span>
+  </li>
+  
+</ul>