Estrazione di codice da termini della Minimalist Type Theory

L’obiettivo di questa tesi è stato l’implementazione di un estrattore di codice per un dimostratore interattivo basato sulla minimalist two-level foundation (mTT), proposta da Maietti. Per raggiungere lo scopo, si è preso a modello l’estrattore di codice del dimostratore Coq ed è stato necessario acquisire conoscenze nell’ambito dell’eliminazione di codice inutile, la quale si occupa di rilevare tramite analisi statica quelle parti di codice che, se eliminate, lasciano invariato l’output riducendo l’uso di RAM e i passi di computazione del programma. L’estrattore è stato implementato utilizzando il linguaggio λProlog, nel quale erano già stati prodotti precedentemente un type checker e una versione provvisoria del compilatore per mTT da Alberto Fiori e Giacomo Molinari nelle loro rispettive tesi. L’interprete di λProlog che ho utilizzato durante il mio lavoro è ELPI, realizzato presso l’Università di Bologna. Pur avendo avuto a disposizione risorse estensive su cui basare l’implementazione, è stato comunque necessario produrre un numero consistente di soluzioni originali: infatti, l’operazione di estrazione richiede spesso un adattamento o, in alcuni casi, una riscrittura dei procedimenti di manipolazione standard sulla base delle differenti idiosincrasie della fondazione logica di partenza. L’estrattore prodotto come risultato finale del lavoro di tesi è completamente funzionante e in grado di estrarre ogni costrutto del livello intensionale della logica mTT, traducendolo in codice OCaml e Haskell.