34 citations · 144 across the 66 of their papers we have counts for
Showing 2013Show all
2 papers · 1 filter
cs.LO2013
Normalisation of a Non-deterministic Type Isomorphic λ-calculus
Alejandro Díaz-Caro, Gilles Dowek
We provide a proof of strong normalisation for lambda+, a recently introduced, explicitly typed, non-deterministic lambda-calculus where isomorphic propositions are identified. Suc…
cs.LO2013★ 4 cited
Non determinism through type isomorphism
Alejandro Díaz-Caro, Gilles Dowek
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-de…