A deconstruction of non-deterministic classical cut elimination

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications
Subtitle of host publicationProceedings of 5th International Conference, TLCA 2001 Kraków, Poland, May 2–5, 2001
EditorsS. Abramsky
Place of PublicationBerlin, Germany
PublisherSpringer Verlag
Pages268-282
Number of pages15
ISBN (Print)9783540419600
DOIs
Publication statusPublished - 2001
Event5th International Conference on Typed Lambda Calculi and Applications, TLCA 2001 - Krakow, Poland
Duration: 2 May 20015 May 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2044

Conference

Conference5th International Conference on Typed Lambda Calculi and Applications, TLCA 2001
CountryPoland
CityKrakow
Period2/05/015/05/01

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'A deconstruction of non-deterministic classical cut elimination'. Together they form a unique fingerprint.

Cite this