A new graphical calculus of proofs

Sandra Alves
(University of Porto)
Maribel Fernández
(King's College London)
Ian Mackie
(Ecole Polytechnique)

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.

In Rachid Echahed: Proceedings 6th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2011), Saarbrücken, Germany, 2nd April 2011, Electronic Proceedings in Theoretical Computer Science 48, pp. 69–84.
Published: 11th February 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.48.8 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org