- 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: +
+ +The execution in the executable formalization has been compared + to real world execution using the USB SPYDER08 + in-circuit debugger. +
+ ++ The code (in OCaml) + of an executable emulator, + automatically generated from the scripts above. On the tests above, + it runs at about 29% of the speed of the + CodeWarrior + emulation engine. +
+ +The formalization has been the Undergraduate Thesis of + Mr. Cosimo Oliboni. The manuscript (italian only) can be found + + 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. +
+ ++ The script present:
+The development requires the SVN version of Matita to be executed.
+