Proof nets sequentialisation in multiplicative linear logic

Abstract. 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 sequential edges, which express the sequentiality constraints given by sequent calculus.

• Type: Journal
• Year: 2008
• Where: APAL
• Authors: Paolo Di Giamberardino, Claudia Faggian
• Keywords: APAL 2008, Proof Net, Sequent Calculus, Sequent Calculus Proof