1 <!--#include virtual="xhtml-header.shtml" -->
3 <html xmlns="http://www.w3.org/1999/xhtml">
5 <title>Matita - Library</title>
6 <!--#include virtual="xhtml-meta.shtml" -->
9 <!--#include virtual="menubar.shtml" -->
11 <h1>Matita Library</h1>
13 <h2>Scripts<a name="scripts"></a></h2>
15 The <a href="nlibrary/">scripts</a> used to generate the knowledge base of
16 Matita can be <a href="nlibrary/">browsed on line</a>.
19 (Old <a href="library/">scripts</a> used in the previous releases of
20 Matita are <a href="library/">still available</a>.)
25 <h1>Large Developments</h1>
27 <h2>Certified Complexity (CerCo)<a name="cerco"></a></h2>
28 <p>Matita is being used to certify a cost preserving compiler from a
29 large subset of C into the 8051 machine code. The compiler does not
30 only produce the target code, but it also instruments the source code
31 with precise cost declarations for the execution of O(1) code
32 fragments. This induced cost model for the source language is
33 inherently non compositional since it is affected by the compilation
34 strategy: the same instructions are compiled in different ways in
35 different contexts, yielding different costs.
37 <p>The final aim of the CerCo project is to formally reason on
38 intensional properties on the C code -- e.g. to show that some hard
39 deadline is always met
40 -- and to be sure that the property holds also for the target code.
42 <p>The CerCo project is a FET Open IST project funded by the EU
43 community in the 7th Framework Programme. More informations on the
44 project and the code of the Matita formalization can be found
45 on the <a href="cerco.cs.unibo.it">CerCo Web site</a>
48 <h2>The Basic Picture<a name="sambin"></a></h2>
50 The <a href="library/formal_topology">scripts</a> present a formalization
51 of some results from the forthcoming book <a href="http://www.oup.com/us/catalog/general/subject/Mathematics/Logic/?view=usa&ci=9780199232888">The Basic Picture - Structures for Constructive Topology</a> by Giovanni Sambin.
53 <p>The formalization has been the result of a three years long
54 collaboration between mathematicians from the University of Padova
55 and computer scientists from the University of
56 Bologna, funded by the University of Padova. In particular,
57 the groups that collaborated are headed respectively by Prof. Sambin
58 in Padua (formal topology and constructive type theory)
59 and by Prof. Asperti in Bologna (constructive type theory and interactive
63 In particular the <a href="library/formal_topology">scripts</a> present:
66 <li>the category of Basic Pairs, that are generalizations of
67 topological spaces</li>
68 <li>the category of Basic Topologies, that are generalizations of
69 formal topologies</li>
70 <li>the existence of a categorical embedding of the former category
71 into the latter. The embedding is an improvement on the usual
72 adjunction between topological spaces and locales</li>
75 All the results are presented constructively and in the predicative
76 fragment of Matita based on the minimalist type theory
77 by Maietti and Sambin, where choice axioms are not valid.
79 In order to reason comfortably on the previous concrete categories and
80 functors, we also present algebraic versions of all the introduced
81 notions, as well as categorical embedding of the concrete categories in
82 the algebrized ones. In particular we formalized:
85 <li>the large category of Overlap Algebras, that extends locales with an
86 axiomatized (= algebraized) overlap binary predicate. The
87 concrete overlap predicate states positively
88 (i.e. without using negation) the existence (in the intuitionistic
89 sense) of a point in the intersection of two sets.
90 Morphisms of Overlap Algebras algebrize concrete relations between
91 sets by means of four functions that capture the
92 existential and universal pre and post images of a relation.
94 <li>the large category of O-Basic Pairs, that algebraize Basic
95 Pairs by means of Overlap Algebras</li>
96 <li>the large category of O-Basic Topologies, that algebraize Basic
97 Topologies by means of Overlap Algebras</li>
98 <li>the categorical embedding of Basic Pairs into O-Basic Pairs and
99 of Basic Topologies into O-Basic Topologies</li>
100 <li>the existence of a categorical embedding of the category
101 of O-Basic Pairs into the category of O-Basic Topologies</li>
104 More information will be available in a forthcoming paper by
105 Claudio Sacerdoti Coen and Enrico Tassi to be
106 published in the Mathematical Structures in Computer Science journal.
109 <h2>Freescale<a name="freescale"></a></h2>
111 The <a href="freescale/">scripts</a> present:
115 <li>an executable formalization of the operational semantics of
116 any <a href="http://www.freescale.com">Freescale</a>
117 micro-controller of the <a href="http://www.freescale.com/webapp/sps/site/homepage.jsp?nodeId=0162468449&tid=FSH">HC05/HC08/RS08/HCS08 families</a>
119 <li>a compiler from assembly language (pseudocodes + operands) to
121 <li>several automatic checks for unhandled opcodes, memory accesses,
122 correctness of ALU logic, etc.</li>
123 <li>three examples of assembly programs (string reverse, counting sort
124 and perfect numbers sieve) with sets of data to run them</li>
127 <p>The execution in the executable formalization has been compared
128 to real world execution using the <a href="http://www.freescale.com/webapp/sps/site/overview.jsp?code=784_LPBBNEWTOOL&fsrch=1">USB SPYDER08</a>
133 The code (in <a href="http://caml.inria.fr">OCaml</a>)
134 of an executable <a href="freescale/freescale_ocaml">emulator</a>,
135 automatically generated from the scripts above. On the tests above,
136 it runs at about 29% of the speed of the
137 <a href="http://www.freescale.com/codewarrior">CodeWarrior</a>
141 <p>The formalization has been the Undergraduate Thesis of
142 Mr. Cosimo Oliboni. The manuscript (italian only) can be found
143 <a href="http://matita.cs.unibo.it/documentation.shtml#freescale">
147 <h2>The Formal System λδ (lambda_delta)<a name="lambda_delta"></a></h2>
149 <p>The formal system λδ is a typed λ-calculus that
150 pursues the unification of terms, types, environments and contexts
152 λδ takes some features from the Automath-related
153 λ-calculi and some from the pure type systems, but differs
154 from both in that it does not include the Π construction while it
155 provides for an abbreviation mechanism at the level of terms.
158 <p> The development presents the proofs of some important properties that
159 λδ enjoys. In particular:
160 <ul> <li> the confluence of reduction </li>
161 <li> the correctness of types </li>
162 <li> the uniqueness of types up to conversion </li>
163 <li> the subject reduction of the type assignment </li>
164 <li> the strong normalization of the typed terms </li>
165 <li> the decidability of type inference problem </li>
170 See the <a href="http://lambda-delta.info/">λδ home page</a>
171 for more information.
174 <h1>Small Developments</h1>
176 <h2>Pointed regular expressions<a name="freescale"></a></h2>
178 The <a href="re/">script</a> present:
182 <li>a formalization of the syntax and semantics of pointed regular
183 expressions, that are regular expressions where points are put
184 in front of atoms to describe where the next character recognized
185 by the expression should be. Multiple points represent the union
186 of multiple languages. A pointed regular expression corresponds
187 to a state of a regular automaton for the regular expression
188 obtained erasing all points.</li>
189 <li>a formalization of the construction of the automaton for a regular
190 expression by means of iterative computation of pointed regular
192 <li>a proof of correctness of the construction (to be completed)</li>
195 <p>The development requires the SVN version of Matita to be executed.</p>
197 <!--#include virtual="bottombar.shtml" -->