TY - GEN
T1 - A deconstruction of non-deterministic classical cut elimination
AU - Laird, J.
PY - 2001
Y1 - 2001
N2 - This paper shows how a symmetric and non-deterministic cut elimination procedure for a classical sequent calculus can be faithfully simulated using a non-deterministic choice operator to combine different 'double-negation' translations of each cut. The resulting interpretation of classical proofs in a λ-calculus with non-deterministic choice leads to a simple proof of termination for cut elimination.
AB - This paper shows how a symmetric and non-deterministic cut elimination procedure for a classical sequent calculus can be faithfully simulated using a non-deterministic choice operator to combine different 'double-negation' translations of each cut. The resulting interpretation of classical proofs in a λ-calculus with non-deterministic choice leads to a simple proof of termination for cut elimination.
UR - http://www.scopus.com/inward/record.url?scp=2942559916&partnerID=8YFLogxK
UR - http://dx.doi.org/10.1007/3-540-45413-6_22
U2 - 10.1007/3-540-45413-6_22
DO - 10.1007/3-540-45413-6_22
M3 - Chapter in a published conference proceeding
AN - SCOPUS:2942559916
SN - 9783540419600
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 268
EP - 282
BT - Typed Lambda Calculi and Applications
A2 - Abramsky, S.
PB - Springer Verlag
CY - Berlin, Germany
T2 - 5th International Conference on Typed Lambda Calculi and Applications, TLCA 2001
Y2 - 2 May 2001 through 5 May 2001
ER -