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
References in corpus (6)
- Linearity in the non-deterministic call-by-value setting
- Call-by-value non-determinism in a linear logic type discipline
- A System F accounting for scalars
- A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
- Completeness of algebraic CPS simulations
- Confluence via strong normalisation in an algebraic λ-calculus with rewriting