Sound and Complete Typing for lambda-mu
In this paper we define intersection and union type assignment for Parigot's calculus lambda-mu. We show that this notion is complete (i.e. closed under subject-expansion), and show also that it is sound (i.e. closed under subject-reduction). This implies that this notion of intersection-union...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2011-01-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1101.4425v1 |
| _version_ | 1818128162933964800 |
|---|---|
| author | Steffen van Bakel |
| author_facet | Steffen van Bakel |
| author_sort | Steffen van Bakel |
| collection | DOAJ |
| description | In this paper we define intersection and union type assignment for Parigot's calculus lambda-mu. We show that this notion is complete (i.e. closed under subject-expansion), and show also that it is sound (i.e. closed under subject-reduction). This implies that this notion of intersection-union type assignment is suitable to define a semantics. |
| first_indexed | 2024-12-11T07:28:52Z |
| format | Article |
| id | doaj.art-4ef3c1d313294f3b86d17288dd330435 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-11T07:28:52Z |
| publishDate | 2011-01-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-4ef3c1d313294f3b86d17288dd3304352022-12-22T01:15:53ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-01-0145Proc. ITRS 2010314410.4204/EPTCS.45.3Sound and Complete Typing for lambda-muSteffen van BakelIn this paper we define intersection and union type assignment for Parigot's calculus lambda-mu. We show that this notion is complete (i.e. closed under subject-expansion), and show also that it is sound (i.e. closed under subject-reduction). This implies that this notion of intersection-union type assignment is suitable to define a semantics.http://arxiv.org/pdf/1101.4425v1 |
| spellingShingle | Steffen van Bakel Sound and Complete Typing for lambda-mu Electronic Proceedings in Theoretical Computer Science |
| title | Sound and Complete Typing for lambda-mu |
| title_full | Sound and Complete Typing for lambda-mu |
| title_fullStr | Sound and Complete Typing for lambda-mu |
| title_full_unstemmed | Sound and Complete Typing for lambda-mu |
| title_short | Sound and Complete Typing for lambda-mu |
| title_sort | sound and complete typing for lambda mu |
| url | http://arxiv.org/pdf/1101.4425v1 |
| work_keys_str_mv | AT steffenvanbakel soundandcompletetypingforlambdamu |