Formalizzazione e Correttezza di algoritmi di ordinamento in Agda​

This report studies the implementation and correctness proof of some sorting algorithms with the employment of Agda, a functional programming language enriched with the classic features of a Proof Assistant. This is done by writing a program in which the proof that that certifies its correct functioning is self contained. The use of software like this gives the advantage of allowing to carry out proofs that are similarly structured to those written by hand, where their correctness is always guaranteed, however. The topics are firstly addressed by introducing the elements used to describe the language functionality in an exhaustive manner. Then, they are put together as the foundation for creating data structures, properties and common libraries, necessary in order to present the case studies.

In questa relazione si studiano l'implementazione e la dimostrazione di correttezza di alcuni algoritmi di ordinamento con l'ausilio di Agda, un linguaggio di programmazione funzionale arricchito delle funzionalità classiche di un Proof Assistant. Ciò si traduce nell'atto di scrivere un programma in cui la prova che ne certifica il corretto funzionamento è auto contenuta. L'impiego di software come questo offre il vantaggio di realizzare prove strutturate in maniera simile a quelle scritte a mano, la cui correttezza è però sempre garantita. Le tematiche vengono affrontate prima introducendo gli elementi utili a descrivere in maniera esaustiva le caratteristiche del linguaggio. Essi sono quindi impiegati come fondamento per la creazione di strutture dati, proprietà e librerie comuni necessarie per la presentazione dei casi di studio.