Matita Library
Scripts
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.)
Large Developments
Certified Complexity (CerCo)
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 Basic Picture
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:
- the category of Basic Pairs, that are generalizations of topological spaces
- the category of Basic Topologies, that are generalizations of formal topologies
- the existence of a categorical embedding of the former category into the latter. The embedding is an improvement on the usual adjunction between topological spaces and locales
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:- the large category of Overlap Algebras, that extends locales with an axiomatized (= algebraized) overlap binary predicate. The concrete overlap predicate states positively (i.e. without using negation) the existence (in the intuitionistic sense) of a point in the intersection of two sets. Morphisms of Overlap Algebras algebrize concrete relations between sets by means of four functions that capture the existential and universal pre and post images of a relation.
- the large category of O-Basic Pairs, that algebraize Basic Pairs by means of Overlap Algebras
- the large category of O-Basic Topologies, that algebraize Basic Topologies by means of Overlap Algebras
- the categorical embedding of Basic Pairs into O-Basic Pairs and of Basic Topologies into O-Basic Topologies
- the existence of a categorical embedding of the category of O-Basic Pairs into the category of O-Basic Topologies
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.
Freescale
The scripts present:
- 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
- several automatic checks for unhandled opcodes, memory accesses, 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
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 λδ (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.
Small Developments
Pointed regular expressions
The script present:
- a formalization of the syntax and semantics of pointed regular expressions, that are regular expressions where points are put in front of atoms to describe where the next character recognized by the expression should be. Multiple points represent the union of multiple languages. A pointed regular expression corresponds to a state of a regular automaton for the regular expression obtained erasing all points.
- a formalization of the construction of the automaton for a regular expression by means of iterative computation of pointed regular expressions.
- a proof of correctness of the construction (to be completed)
The development requires the SVN version of Matita to be executed.
