Concept

Matita

Matita is an experimental proof assistant under development at the Computer Science Department of the University of Bologna. It is a tool aiding the development of formal proofs by man-machine collaboration, providing a programming environment where formal specifications, executable algorithms and automatically verifiable correctness certificates naturally coexist. Matita is based on a dependent type system known as the Calculus of (Co)Inductive Constructions (a derivative of Calculus of Constructions), and is compatible, to some extent, with Coq. The word "matita" means "pencil" in Italian (a simple and widespread editing tool). It is a reasonably small and simple application, whose architectural and software complexity is meant to be mastered by students, providing a tool particularly suited for testing innovative ideas and solutions. Matita adopts a tactic-based editing mode; (XML-encoded) proof objects are produced for storage and exchange. Existential variables are native in Matita, allowing a simpler management of dependent goals. Matita implements a bidirectional type inference algorithm exploiting both inferred and expected types. The power of the type inference system (refiner) is further augmented by a mechanism of hints that helps in synthesizing unifiers in particular situations specified by the user. Matita supports a sophisticated disambiguation strategy based on a dialog between the parser and the typechecker. At the interactive level, the system implements a small step execution of structured tactics allowing a much better management of the proof development, and naturally leading to more structured and readable scripts. Matita has been employed in CerCo (Certified Complexity): a FP7 European Project focused on the development of a formally verified, complexity preserving compiler from a large subset of C to the assembler of a MCS-51 microprocessor. The Matita tutorial provides a pragmatic introduction to the main functionalities of the Matita interactive theorem prover, offering a guided tour through a set of non-trivial examples in the field of software specification and verification.

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.