A new graphical calculus of proofs

TL;DR

This paper introduces a novel graphical calculus for intuitionistic logic proofs, inspired by proof nets and interaction nets, providing an intuitive visual framework that also applies to lambda calculus computations.

Contribution

It presents a new graphical representation that combines features of proof nets and interaction nets, extending their applicability and simplifying proof visualization.

Findings

Provides a simple, intuitive graphical calculus for proofs

Extends applicability to lambda calculus representations

Retains beneficial features of proof nets and interaction nets

Abstract

We offer a simple graphical representation for proofs of intuitionistic logic, which is inspired by proof nets and interaction nets (two formalisms originating in linear logic). This graphical calculus of proofs inherits good features from each, but is not constrained by them. By the Curry-Howard isomorphism, the representation applies equally to the lambda calculus, offering an alternative diagrammatic representation of functional computations.