X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=9874142c96d59067111f30163cc1e4ca4dfddfb8;hb=a9355590f890b133763a1593fa706c0631e2c241;hp=3c4246f313b566485c3bf0ec9180281e0221b06b;hpb=708e70e2b90c71c9caedef2665a8d4971cf7b8d9;p=helm.git diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml index 3c4246f31..9874142c9 100644 --- a/helm/www/matita/library.shtml +++ b/helm/www/matita/library.shtml @@ -15,11 +15,94 @@ 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, sponsored 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, without any reference to choice axioms. +
+ In order to reason conformtably 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 algebraized 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: @@ -85,6 +168,29 @@ for more information.
++ The script present: +
+ +The development requires the SVN version of Matita to be executed.
+