X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=d065b7a9f643a104aac62d96577f14daf08ea5d7;hb=23fa9e70972efb0a805a4fecf6c91103f42408f2;hp=c22db5e1ce9f03802dcbcb812811ff85175bef68;hpb=ecf6f2741d56261acf4580379d35117d80385da2;p=helm.git diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml index c22db5e1c..d065b7a9f 100644 --- a/helm/www/matita/library.shtml +++ b/helm/www/matita/library.shtml @@ -12,14 +12,100 @@
- The scripts used to generate the knowledge base of - Matita can be browsed on line. + The scripts used to generate the knowledge base of + Matita can be browsed on line. +
++ (Old scripts used in the previous releases of + Matita are still available.)
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 +144,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.
+