Normalisation of a Non-deterministic Type Isomorphic {\lambda}-calculus

TL;DR

This paper proves strong normalization for lambda+, a non-deterministic, explicitly typed lambda-calculus that identifies isomorphic propositions, using an adapted reducibility candidates technique.

Contribution

It provides the first strong normalization proof for lambda+, incorporating isomorphic propositions and non-determinism.

Findings

Lambda+ is strongly normalizing.

Isomorphic propositions are effectively handled.

The reducibility candidates technique is successfully adapted.

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.