@inproceedings{aef6dcf5318b466bbc550c771b754298,
title = "Confluence of cut-elimination procedures for the intuitionistic sequent calculus",
abstract = "We prove confluence of two cut-elimination procedures for the implicational fragment of a standard intuitionistic sequent calculus. One of the cut-elimination procedures uses global proof transformations while the other consists of local ones. Both of them include permutation of cuts to simulate β-reduction in an isomorphic image of the λ-calculus. We establish the confluence properties through a conservativity result on the cut-elimination procedures.",
keywords = "λ-calculus, Confluence, Cut-elimination, Explicit substitution, Sequent calculus",
author = "Kentaro Kikuchi",
year = "2007",
doi = "10.1007/978-3-540-73001-9_41",
language = "English",
isbn = "9783540730002",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "398--407",
booktitle = "Computation and Logic in the Real World - Third Conference on Computability in Europe, CiE 2007, Proceedings",
note = "3rd Conference on Computability in Europe, CiE 2007 ; Conference date: 18-06-2007 Through 23-06-2007",
}