Bibtex de la publication

@InProceedings{ Es2014.2,
author = {Espírito Santo, José and Matthes, Ralph and Nakazawa, Koji and Pinto, Luís},
title = "{Confluence for classical logic through the distinction between values and computations (regular paper)}",
booktitle = "{International Workshop on Classical Logic and Computation (CL&C 2014), Vienne, 13/07/14}",
editor = {van Bakel, Steffen and Berardi, Stefano and Oliva, Paulo},
year = {2014},
month = {septembre},
publisher = {Electronic Proceedings in Theoretical Computer Science},
address = {},
volume = {164},
pages = {63--77},
language = {anglais},
URL = {},
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.}