Formalizzazione di una rappresentazione canonica dello sharing per la valutazione call-by-value

Data la sua definizione di alto livello, lambda-calcolo è spesso considerato un formalismo poco adatto agli studi di complessità: solo di recente in letteratura sono state sviluppate implementazioni del lambda-calcolo con un overhead ragionevole nel numero di riduzioni necessarie per normalizzare il termine. Una famiglia di queste implementazioni è quella delle crumbling abstract machines; esse lavorano su termini arricchiti da un costrutto di sharing che permette di ritardare quanto più possibile le riscritture dei termini e da mantenere basso l'overhead della valutazione. Il corretto funzionamento di queste macchine si fonda su numerosi risultati che è stato utile dimostrare formalmente. In questo lavoro, dopo aver descritto sommariamente il lambda-calcolo e la teoria delle crumbling abstract machines, descriveremo come è stata formalizzata la fase di inizializzazione di queste macchine soffermandoci su alcuni risultati che, non dimostrandosi validi, hanno dovuto essere almeno in parte riformulati e dimostrati corretti. Il lavoro complessivo ha avuto esito positivo: tutti i risultati formalizzati si sono corretti o, altrimenti, è stato possibile formulare e dimostrare enunciati che permettessero di sostituire quelli che si sono verificati non validi.