Confluence for classical logic through the distinction between values and computations

José Espírito Santo
Ralph Matthes
Koji Nakazawa
Luís Pinto

We apply an idea originated in the theory of programming languages - monadic meta-language with a distinction between values and computations - in the design of a calculus of cut-elimination for classical logic. The cut-elimination calculus we obtain comprehends the call-by-name and call-by-value fragments of Curien-Herbelin's lambda-bar-mu-mu-tilde-calculus without losing confluence, and is based on a distinction of "modes" in the proof expressions and "mode" annotations in types. Modes resemble colors and polarities, but are quite different: we give meaning to them in terms of a monadic meta-language where the distinction between values and computations is fully explored. This meta-language is a refinement of the classical monadic language previously introduced by the authors, and is also developed in the paper.

In Paulo Oliva: Proceedings Fifth International Workshop on Classical Logic and Computation (CL&C 2014), Vienna, Austria, July 13, 2014, Electronic Proceedings in Theoretical Computer Science 164, pp. 63–77.
Published: 9th September 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.164.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org