Normalisation of a Non-deterministic Type Isomorphic {λ}-calculus
classification
💻 cs.LO
keywords
isomorphiclambdanon-deterministicnormalisationproofadaptationcalculuscandidates
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.