X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=3c4246f313b566485c3bf0ec9180281e0221b06b;hb=52e5fe4592c61448edfd406a396c9fa9ab7e2e46;hp=a6f195b630f6c9f6eed33b9df899c8323de49fee;hpb=9d356a6f202a77fb1dd67b57b1c86ac3ebe1382b;p=helm.git
diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index a6f195b63..3c4246f31 100644
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -1,6 +1,6 @@
-
-
+
+
Matita - Library
@@ -29,14 +29,14 @@
an executable formalization of the operational semantics of
any Freescale
micro-controller of the HC05/HC08/RS08/HCS08 families
+
a compiler from assembly language (pseudocodes + operands) to
- machine code
+ machine code
several automatic checks for unhandled opcodes, memory accesses,
- correctness of ALU logic, etc.
+ correctness of ALU logic, etc.
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
-
The execution in the executable formalization has been compared
to real world execution using the USB SPYDER08
@@ -58,6 +58,33 @@
here.
+ The Formal System λδ (lambda-delta)
+
+ The formal system λδ is a typed λ-calculus that
+ pursues the unification of terms, types, environments and contexts
+ as the main goal.
+ λδ takes some features from the Automath-related
+ λ-calculi and some from the pure type systems, but differs
+ from both in that it does not include the Π construction while it
+ provides for an abbreviation mechanism at the level of terms.
+
+
+ The development presents the proofs of some important properties that
+ λδ enjoys. In particular:
+
- the confluence of reduction
+ - the correctness of types
+ - the uniqueness of types up to conversion
+ - the subject reduction of the type assignment
+ - the strong normalization of the typed terms
+ - the decidability of type inference problem
+
+
+
+
+ See the λδ home page
+ for more information.
+
+