Non determinism through type isomorphism
arXiv:1303.7334 · doi:10.4204/EPTCS.113.13
Abstract
We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-deterministic and algebraic lambda-calculi.
In Proceedings LSFA 2012, arXiv:1303.7136