Introduction to linear logic and ludics, part II

TL;DR

This paper introduces proof nets within multiplicative linear logic and explores ludics, emphasizing their roles in understanding the interactive nature of computation and logic, with insights relevant to computer science.

Contribution

It provides an overview of proof nets in multiplicative linear logic and discusses recent developments in ludics, highlighting their significance in computational interaction.

Findings

Proof nets clarify the structure of multiplicative linear logic.

Ludics reveals the interactive essence of computation and logic.

The paper offers computer science insights into ludics' theoretical framework.

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.