Normalisation of a Non-deterministic Type Isomorphic {\lambda}-calculus
Logic in Computer Science
2014-01-09 v3
Abstract
We provide a proof of strong normalisation for lambda+, a recently introduced, explicitly typed, non-deterministic lambda-calculus where isomorphic propositions are identified. Such a proof is a non-trivial adaptation of the reducibility candidates technique.
Keywords
Cite
@article{arxiv.1306.5089,
title = {Normalisation of a Non-deterministic Type Isomorphic {\lambda}-calculus},
author = {Alejandro Díaz-Caro and Gilles Dowek},
journal= {arXiv preprint arXiv:1306.5089},
year = {2014}
}
Comments
This paper has been withdrawn by the authors due to a crucial error in Definition 1