Software verification and Interactive Theorem Proving

Mechanized mathematical proofs are becoming a standard tool in research related to programming languages and software development methods. In particular, proof assistants based on dependent type theory seem to enjoy a growing popularity in this field, due to several attractive features of these formalisms:

• type theories embed key computational constructs of functional programming languages: functions can be defined by (well-founded) recursion, and are live entities that can be tested and executed; data are typed terms identified modulo reduction to their normal form (conversion), allowing to distinguish between computation and reasoning, and to treat them differently (sometimes referred to as ``Poincaré principle''); the more powerful is the conversion rule, the more reasoning is reduced to mere computation, making the logical argument more concise and cogent;
• proofs are an integrated part of the formalism, allowing, via the Curry Howard isomorphism, a smooth interplay between specification and reasoning: proofs are objects of the language, and can be treated as normal data, naturally leading to a programming style akin to proof-carrying-code, where chunks of software come equipped with proofs of (some of) their properties. Moreover, sharing a common syntax between the logical and the computational part of the theory reduces verification to type-checking, in such a way that only a small and well-identified software component (the kernel) is really critical for the reliability of the whole application (the so-called ``de Bruijn principle'').

The tutorial will introduce the above mentioned methodologies and techniques making using of a recent tool for the mechanization of formal reasoning called Matita.