Confluence for classical logic through the distinction between values and computations

TL;DR

This paper introduces a new calculus for classical logic that incorporates a distinction between values and computations, inspired by programming language theory, ensuring confluence and covering multiple evaluation strategies.

Contribution

It extends monadic meta-language concepts to classical logic proof calculus, enabling a unified, confluent cut-elimination framework with mode annotations.

Findings

Achieves confluence in the calculus for classical logic

Unifies call-by-name and call-by-value fragments

Introduces mode annotations with a monadic interpretation

Abstract

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.