Estrazione di codice da termini della Minimalist Type Theory

Caprari, Riccardo (2018) Estrazione di codice da termini della Minimalist Type Theory. [Laurea magistrale], Università di Bologna, Corso di Studio in Informatica [LM-DM270]
Documenti full-text disponibili:
[img] Documento PDF (Thesis)
Disponibile con Licenza: Creative Commons Attribuzione - Non commerciale - Condividi allo stesso modo 3.0

Download (346kB)

Abstract

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.

Abstract
Tipologia del documento
Tesi di laurea (Laurea magistrale)
Autore della tesi
Caprari, Riccardo
Relatore della tesi
Scuola
Corso di studio
Indirizzo
CURRICULUM A: TECNICHE DEL SOFTWARE
Ordinamento Cds
DM270
Parole chiave
Estrazione di codice,Lambda Prolog,Dimostratore interattivo,Teoria dei tipi
Data di discussione della Tesi
20 Dicembre 2018
URI

Altri metadati

Statistica sui download

Gestione del documento: Visualizza il documento

^