English

Why the usual candidates of reducibility do not work for the symmetric $\lambda\mu$-calculus

Logic 2009-05-12 v1

Abstract

The symmetric λmu\lambda mu-calculus is the λμ\lambda\mu-calculus introduced by Parigot in which the reduction rule μ\mu', which is the symmetric of μ\mu, is added. We give examples explaining why the technique using the usual candidates of reducibility does not work. We also prove a standardization theorem for this calculus.

Keywords

Cite

@article{arxiv.0905.1554,
  title  = {Why the usual candidates of reducibility do not work for the symmetric $\lambda\mu$-calculus},
  author = {René David and Karim Nour},
  journal= {arXiv preprint arXiv:0905.1554},
  year   = {2009}
}

Comments

Second Workshop on Computational Logic and Applications (CLA 2004), France (2004)