Proof nets sequentialisation in Multiplicative Linear Logic


Paolo Di Giamberardino, Claudia Faggian

Annals of Pure and Applied Logic 155 (3):173-182


We provide an alternative proof of the sequentialisation theorem for proof nets of multiplicative linear logic. Namely, we show how a proof net can be transformed into a sequent calculus proof simply by properly adding to it some special edges, called \emph{sequential edges}, which express the sequentiality constraints given by sequent calculus.

Download: apal08.pdf