Intersection Subtyping with Constructors
We study the question of extending the BCD intersection type system with additional type constructors. On the typing side, we focus on adding the usual rules for product types. On the subtyping side, we consider a generic way of defining a subtyping relation on families of types which include inters...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2019-04-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1904.10108v1 |
| _version_ | 1818270820706811904 |
|---|---|
| author | Olivier Laurent |
| author_facet | Olivier Laurent |
| author_sort | Olivier Laurent |
| collection | DOAJ |
| description | We study the question of extending the BCD intersection type system with additional type constructors. On the typing side, we focus on adding the usual rules for product types. On the subtyping side, we consider a generic way of defining a subtyping relation on families of types which include intersection types. We find back the BCD subtyping relation by considering the particular case where the type constructors are intersection, omega and arrow. We obtain an extension of BCD subtyping to product types as another instance. We show how the preservation of typing by both reduction and expansion is satisfied in all the considered cases. Our approach takes benefits from a "subformula property" of the proposed presentation of the subtyping relation. |
| first_indexed | 2024-12-12T21:16:21Z |
| format | Article |
| id | doaj.art-a94a7fd351f84d898269c5ade5b6f4cc |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-12T21:16:21Z |
| publishDate | 2019-04-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-a94a7fd351f84d898269c5ade5b6f4cc2022-12-22T00:11:45ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-04-01293Proc. DCM 2018 and ITRS 2018738410.4204/EPTCS.293.6:4Intersection Subtyping with ConstructorsOlivier Laurent0 Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France We study the question of extending the BCD intersection type system with additional type constructors. On the typing side, we focus on adding the usual rules for product types. On the subtyping side, we consider a generic way of defining a subtyping relation on families of types which include intersection types. We find back the BCD subtyping relation by considering the particular case where the type constructors are intersection, omega and arrow. We obtain an extension of BCD subtyping to product types as another instance. We show how the preservation of typing by both reduction and expansion is satisfied in all the considered cases. Our approach takes benefits from a "subformula property" of the proposed presentation of the subtyping relation.http://arxiv.org/pdf/1904.10108v1 |
| spellingShingle | Olivier Laurent Intersection Subtyping with Constructors Electronic Proceedings in Theoretical Computer Science |
| title | Intersection Subtyping with Constructors |
| title_full | Intersection Subtyping with Constructors |
| title_fullStr | Intersection Subtyping with Constructors |
| title_full_unstemmed | Intersection Subtyping with Constructors |
| title_short | Intersection Subtyping with Constructors |
| title_sort | intersection subtyping with constructors |
| url | http://arxiv.org/pdf/1904.10108v1 |
| work_keys_str_mv | AT olivierlaurent intersectionsubtypingwithconstructors |