Non determinism through type isomorphism
Alejandro D\'iaz-Caro, Gilles Dowek
TL;DR
This paper introduces an equivalence relation on propositions and a proof system where equivalent propositions share proofs, connecting to known non-deterministic and algebraic lambda-calculi.
Contribution
It defines a novel equivalence relation and proof system that unify various non-deterministic lambda-calculi through type isomorphism.
Findings
Establishes an equivalence relation on propositions.
Develops a proof system where equivalent propositions have identical proofs.
Shows resemblance to known non-deterministic lambda-calculi.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.