Non determinism through type isomorphism
Logic in Computer Science
2013-04-01 v1
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.
Cite
@article{arxiv.1303.7334,
title = {Non determinism through type isomorphism},
author = {Alejandro Díaz-Caro and Gilles Dowek},
journal= {arXiv preprint arXiv:1303.7334},
year = {2013}
}
Comments
In Proceedings LSFA 2012, arXiv:1303.7136