Formalizzazione delle proprietà di macchine per la call-by-value in forma normale

La call-by-value è una strategia di valutazione usata in molti ambiti, uno di questi sono le macchine astratte per il Lambda calcolo, dove si è dimostrata efficace nel trattare il caso chiuso adottando weak evaluation. Si riscontra però che risulta problematica se estesa al caso aperto, in particolare nel caso di adozione di strong evaluation. Per ovviare a questo problema esistono in letteratura vari approcci, uno di questi è l’aggiunta di costrutti per lo sharing. Nell’articolo su cui ho lavorato si applica una trasformazione sui termini del λ-calcolo costruendo una coda di sostituzioni esplicite e si studiano le differenze introdotte da questo design rispetto ad altri approcci; si valutano inoltre la correttezza e la complessità relative a questo approccio. Il lavoro svolto consiste nella seconda parte di un progetto di formalizzazione dell articolo ’Crumbling Abstract Machines’ di Accattoli et al. utilizzando il software Matita. Si riportano in Matita le appendici dell’ar- ticolo, nello specifico la sezione 3 riguardante l’implementazione delle Transizioni della macchina GLAM nel caso chiuso, infine si dimostra parzialmente la proprietà di unloading per questa implementazione.