Formalizzazione di proprietà di programmi mediante un proof-assistant

Proof-assistants are interactive software systems that support the formalization and demonstration of mathematical concepts. Unlike automated theorem provers, proof-assistants focus on the verification of a given proof, ensuring the correctness of the respective theorem. One such system, Lean, is a functional programming language based on dependent type theory. This thesis is divided into two parts: the first provides an introduction to how Lean works and the ideas that allow its use as a proof-assistant, in the second Lean is used to support the formalization and analysis of IMP, a minimal imperative programming language, in the formulation described by Nipkow and Klein. Within the proof-assistant, two different, albeit demonstrably equivalent, formulations of the semantics are defined. The semantics support the formalization of two type systems, each of which statically guarantees a desired property of programs: in the first case the absence of errors due to incompatible data combinations, in the second a particular security property about the absence of information flows from private data to public observers. The result of the project is the complete coding and verification in Lean of the above results.

I proof-assistant sono sistemi software interattivi di supporto alla formalizzazione e alla dimostrazione di concetti matematici. A differenza dei sistemi di dimostrazione automatica, i proof-assistant si concentrano sulla verifica di una dimostrazione data, garantendo la correttezza del rispettivo teorema. Uno di questi sistemi, Lean, è un linguaggio di programmazione funzionale basato sulla teoria dei tipi dipendenti. La tesi è suddivisa in due parti: la prima fornisce un'introduzione al funzionamento di Lean e alle idee che ne permettono l'utilizzo come proof-assistant, nella seconda Lean è usato a supporto della formalizzazione e analisi di IMP, un linguaggio di programmazione imperativo minimale, nella formulazione descritta da Nipkow e Klein. Entro il proof-assistant, ne vengono definite due differenti, seppur dimostrabilmente equivalenti, formulazioni della semantica. Le semantiche fungono da supporto alla formalizzazione di due sistemi di tipi, ciascuno dei quali garantisce staticamente una proprietà desiderata dei programmi: nel primo caso l'assenza di errori dovuti a combinazioni di dati incompatibili, nel secondo una particolare proprietà di sicurezza circa l'assenza di flussi di informazioni da dati privati verso osservatori pubblici. Risultato del progetto è la completa codifica e verifica in Lean dei suddetti risultati.