Cari tutti,
il prossimo venerdì 28 Ottobre, alle ore 11:30 in aula 311 (Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1), si terrà il seguente seminario:

Giulio Guerrieri (Università Roma Tre - Université d'Aix-Marseille)
Il !-calcolo: una variante del lambda-calcolo che generalizza la chiamata per nome e la chiamata per valore

Abstract:
Introdurremo e studieremo il !-calcolo, un calcolo funzionale non tipato in cui l'operatore di promozione della Logica Lineare fa esplicitamente parte della sintassi e l'applicazione è bilineare.
Questo calcolo, che può essere visto come una versione non tipata del calcolo Call-By-Push-Value di Paul Levy, sussume sia il lambda-calcolo per nome sia il lambda-calcolo per valore, in quanto consente (e internalizza) una fattorizzazione delle due traduzioni di Girard della logica intuizionista nella Logica Lineare.
Costruiremo un modello denotazionale del !-calcolo basato sulla interpretazione relazionale della Logica Lineare e dimostreremo un teorema di correttezza per tale modello ricorrendo a una versione con risorse del !-calcolo basato sulla Logica Lineare Differenziale.