Correctness Criteria for Second Order Multiplicative Linear Logic
Adrien Ragot, Thomas Seiller, Lorenzo Tortora de Falco · HAL (Le Centre pour la Communication Scientifique Directe) · 2025
We define untyped proof structures for second order multiplicative linear logic as hypergraphs that we call nets. We give a desequentialisation method associating a proof-tree its representing net, and because not all nets represent a proof we define a correctness criterion, based on parsing, which determines (and construct) the proof that is represented by a net S (if such proof exists). Because the parsing rewriting is confluent on proof nets and always decreases the size of a net our criterion runs in quadratic time.