Normalisation of a Non-deterministic Type Isomorphic λ-calculus

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.

arXiv commentThis paper has been withdrawn by the authors due to a crucial error in Definition 1