Non determinism through type isomorphism

DÍAZ-CARO, ALEJANDRO; DOWEK, GILLES

Electronic Proceedings in Theoretical Computer Science

Open Publishing Association

Año: 2013 vol. 113 p. 137 - 144

We define an equivalence relation on propositions and a proof system where equivalent propositionshave the same proofs. The system obtained this way resembles several known non-deterministic andalgebraic lambda-calculi.