Non determinism through type isomorphism

Non determinism through type isomorphism

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.

Bibliographic Details
Main Authors: Alejandro Díaz-Caro, Gilles Dowek
Format: Article
Language:English
Published: Open Publishing Association 2013-03-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1303.7334v1
id doaj-1311c00756bf456ab4c8c2e80de6fd07
record_format Article
spelling doaj-1311c00756bf456ab4c8c2e80de6fd072020-11-24T21:00:02ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-03-01113Proc. LSFA 201213714410.4204/EPTCS.113.13Non determinism through type isomorphismAlejandro Díaz-CaroGilles DowekWe 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.http://arxiv.org/pdf/1303.7334v1
collection DOAJ
language English
format Article
sources DOAJ
author Alejandro Díaz-Caro
Gilles Dowek
spellingShingle Alejandro Díaz-Caro
Gilles Dowek
Non determinism through type isomorphism
Electronic Proceedings in Theoretical Computer Science
author_facet Alejandro Díaz-Caro
Gilles Dowek
author_sort Alejandro Díaz-Caro
title Non determinism through type isomorphism
title_short Non determinism through type isomorphism
title_full Non determinism through type isomorphism
title_fullStr Non determinism through type isomorphism
title_full_unstemmed Non determinism through type isomorphism
title_sort non determinism through type isomorphism
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2013-03-01
description 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.
url http://arxiv.org/pdf/1303.7334v1
work_keys_str_mv AT alejandrodiazcaro nondeterminismthroughtypeisomorphism
AT gillesdowek nondeterminismthroughtypeisomorphism
_version_ 1716780524364627968

Similar Items