Recognition: unknown
Introduction to linear logic and ludics, part II
classification
💻 cs.LO
keywords
logiclinearludicsintroductionpartbeencentralcomputation
read the original abstract
This paper is the second part of an introduction to linear logic and ludics, both due to Girard. It is devoted to proof nets, in the limited, yet central, framework of multiplicative linear logic and to ludics, which has been recently developped in an aim of further unveiling the fundamental interactive nature of computation and logic. We hope to offer a few computer science insights into this new theory.
This paper has not been read by Pith yet.
Forward citations
Cited by 1 Pith paper
-
Metacat: a categorical framework for formal systems
Metacat is a new categorical model for formal systems using spans in cartesian PROPs to encode inference rules and symmetric monoidal categories for proofs, with a proof-checking implementation for FOL.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.