2013/06/21 by Alejandro Díaz-Caro, Gilles Dowek, Díaz-Caro, Alejandro +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.1306.5089
This paper has been withdrawn by the authors due to a crucial error in Definition 1
arxiv created 2014/01/08 · arxiv updated 2014/01/09
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.