Matita Library

Scripts

The scripts used to generate the knowledge base of Matita can be browsed on line.

Large Developments

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.