Aula 311 (Palazzina C, Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1)
Abstract
Le reti di prova sono una sintassi per le prove della logica lineare con una rappresentazione geometrica intuitiva che permette di definire una relazione di equivalenza tra derivazioni meno fine rispetto alla pura equivalenza sintattica.
In questo incontro daremo una sintassi bidimensionale alternativa per le derivazioni della logica lineare moltiplicativa. Nel nostro caso, la sintassi dei diagrammi di corde permette la definizione di un formalismo in cui verificare se un diagramma corrisponde ad una prova può essere verificato in tempo lineare.
Inoltre mostreremo come questa sintassi possa essere utilizzata per definire una semantica denotazionale per la logica lineare moltiplicativa con unità tramite classi di equivalenza di diagrammi (generata da una riscrittura terminante).
