The untyped stack calculus and Bohm's theorem
The stack calculus is a functional language in which is in a Curry-Howard correspondence with classical logic. It enjoys confluence but, as well as Parigot's lambda-mu, does not admit the Bohm Theorem, typical of the lambda-calculus. We present a simple extension of stack calculus which is for...
| Main Author: | |
|---|---|
| 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.7330v1 |
| _version_ | 1819121960946237440 |
|---|---|
| author | Alberto Carraro |
| author_facet | Alberto Carraro |
| author_sort | Alberto Carraro |
| collection | DOAJ |
| description | The stack calculus is a functional language in which is in a Curry-Howard correspondence with classical logic. It enjoys confluence but, as well as Parigot's lambda-mu, does not admit the Bohm Theorem, typical of the lambda-calculus. We present a simple extension of stack calculus which is for the stack calculus what Saurin's Lambda-mu is for lambda-mu. |
| first_indexed | 2024-12-22T06:44:52Z |
| format | Article |
| id | doaj.art-22e27d89f60746c29e857db6a05c1747 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-22T06:44:52Z |
| publishDate | 2013-03-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-22e27d89f60746c29e857db6a05c17472022-12-21T18:35:19ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-03-01113Proc. LSFA 2012779210.4204/EPTCS.113.9The untyped stack calculus and Bohm's theoremAlberto CarraroThe stack calculus is a functional language in which is in a Curry-Howard correspondence with classical logic. It enjoys confluence but, as well as Parigot's lambda-mu, does not admit the Bohm Theorem, typical of the lambda-calculus. We present a simple extension of stack calculus which is for the stack calculus what Saurin's Lambda-mu is for lambda-mu.http://arxiv.org/pdf/1303.7330v1 |
| spellingShingle | Alberto Carraro The untyped stack calculus and Bohm's theorem Electronic Proceedings in Theoretical Computer Science |
| title | The untyped stack calculus and Bohm's theorem |
| title_full | The untyped stack calculus and Bohm's theorem |
| title_fullStr | The untyped stack calculus and Bohm's theorem |
| title_full_unstemmed | The untyped stack calculus and Bohm's theorem |
| title_short | The untyped stack calculus and Bohm's theorem |
| title_sort | untyped stack calculus and bohm s theorem |
| url | http://arxiv.org/pdf/1303.7330v1 |
| work_keys_str_mv | AT albertocarraro theuntypedstackcalculusandbohmstheorem AT albertocarraro untypedstackcalculusandbohmstheorem |