X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=c42fa673bd0fd87dcab5afe1841e23771fdbab47;hb=0c8cad22457218f78c30de239e49187968251613;hp=c22db5e1ce9f03802dcbcb812811ff85175bef68;hpb=ecf6f2741d56261acf4580379d35117d80385da2;p=helm.git diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml index c22db5e1c..c42fa673b 100644 --- a/helm/www/matita/library.shtml +++ b/helm/www/matita/library.shtml @@ -15,11 +15,96 @@ The scripts used to generate the knowledge base of Matita can be browsed on line.
++ The experimental scripts for the next major version of Matita can also be browsed on line. +
Matita is being used to certify a cost preserving compiler from a + large subset of C into the 8051 machine code. The compiler does not + only produce the target code, but it also instruments the source code + with precise cost declarations for the execution of O(1) code + fragments. This induced cost model for the source language is + inherently non compositional since it is affected by the compilation + strategy: the same instructions are compiled in different ways in + different contexts, yielding different costs. +
+The final aim of the CerCo project is to formally reason on + intensional properties on the C code -- e.g. to show that some hard + deadline is always met + -- and to be sure that the property holds also for the target code. +
+The CerCo project is a FET Open IST project funded by the EU + community in the 7th Framework Programme. More informations on the + project and the code of the Matita formalization can be found + on the CerCo Web site +
+ ++ The scripts present a formalization + of some results from the forthcoming book The Basic Picture - Structures for Constructive Topology by Giovanni Sambin. +
+The formalization has been the result of a three years long + collaboration between mathematicians from the University of Padova + and computer scientists from the University of + Bologna, funded by the University of Padova. In particular, + the groups that collaborated are headed respectively by Prof. Sambin + in Padua (formal topology and constructive type theory) + and by Prof. Asperti in Bologna (constructive type theory and interactive + theorem proving). +
++ In particular the scripts present: +
++ All the results are presented constructively and in the predicative + fragment of Matita based on the minimalist type theory + by Maietti and Sambin, where choice axioms are not valid. +
+ In order to reason comfortably on the previous concrete categories and + functors, we also present algebraic versions of all the introduced + notions, as well as categorical embedding of the concrete categories in + the algebrized ones. In particular we formalized: + ++ More information will be available in a forthcoming paper by + Claudio Sacerdoti Coen and Enrico Tassi to be + published in the Mathematical Structures in Computer Science journal. +
+The scripts present: @@ -58,11 +143,56 @@ here.
-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: +
+ See the λδ home page + for more information. +
+ +- See the λδ home page. + The script present:
+The development requires the SVN version of Matita to be executed.
+