Jump from Parallel to Sequential proof: Multiplicatives


Paolo Di Giamberardino, Claudia Faggian

Computer Science Logic 4207:319-333

in Lecture Notes in Computer Science

Springer Berlin / Heidelberg


We introduce a new class of multiplicative proof nets, J-proof nets, which are a typed version of Faggian and Maurel's multiplicative L-nets. In J-proof nets, we can characterize nets with different degrees of sequentiality, by gradual insertion of sequentiality constraints. As a byproduct, we obtain a simple proof of the sequentialisation theorem.

Download: | csl06.pdf