File Download
There are no files associated with this item.
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1007/978-3-031-21037-2_8
- Scopus: eid_2-s2.0-85144400820
- WOS: WOS:000897034100008
Supplementary
- Citations:
- Appears in Collections:
Conference Paper: Applicative Intersection Types
Title | Applicative Intersection Types |
---|---|
Authors | |
Issue Date | 25-Nov-2022 |
Publisher | Springer |
Abstract | Calculi with intersection types have been used over the years to model various features, including: overloading, extensible records and, more recently, nested composition and return type overloading. Never- theless no previous calculus supports all those features at once. In this paper we study expressive calculi with intersection types and a merge operator. Our first calculus supports an unrestricted merge operator, which is able to support all the features, and is proven to be type sound. However, the semantics is non-deterministic. In the second calculus we employ a previously proposed disjointness restriction, to make the se- mantics deterministic. Some forms of overloading are forbidden, but all other features are supported. The main challenge in the design is related to the semantics of applications and record projections. We propose an applicative subtyping relation that enables the inference of result types for applications and projections. Correspondingly, there is an applica- tive dispatching relation that is used for the dynamic semantics. The two calculi and their proofs are formalized in the Coq theorem prover. |
Persistent Identifier | http://hdl.handle.net/10722/338158 |
ISBN | |
ISI Accession Number ID |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Xue, Xu | - |
dc.contributor.author | Dos Santos Oliveira, Bruno Cesar | - |
dc.contributor.author | Xie, Ningning | - |
dc.date.accessioned | 2024-03-11T10:26:41Z | - |
dc.date.available | 2024-03-11T10:26:41Z | - |
dc.date.issued | 2022-11-25 | - |
dc.identifier.isbn | 9783031210365 | - |
dc.identifier.uri | http://hdl.handle.net/10722/338158 | - |
dc.description.abstract | <p>Calculi with intersection types have been used over the years to model various features, including: overloading, extensible records and, more recently, nested composition and return type overloading. Never- theless no previous calculus supports all those features at once. In this paper we study expressive calculi with intersection types and a merge operator. Our first calculus supports an unrestricted merge operator, which is able to support all the features, and is proven to be type sound. However, the semantics is non-deterministic. In the second calculus we employ a previously proposed disjointness restriction, to make the se- mantics deterministic. Some forms of overloading are forbidden, but all other features are supported. The main challenge in the design is related to the semantics of applications and record projections. We propose an applicative subtyping relation that enables the inference of result types for applications and projections. Correspondingly, there is an applica- tive dispatching relation that is used for the dynamic semantics. The two calculi and their proofs are formalized in the Coq theorem prover.</p> | - |
dc.language | eng | - |
dc.publisher | Springer | - |
dc.relation.ispartof | The 20th Asian Symposium on Programming Languages and Systems (05/12/2022-10/12/2022, Auckland) | - |
dc.title | Applicative Intersection Types | - |
dc.type | Conference_Paper | - |
dc.identifier.doi | 10.1007/978-3-031-21037-2_8 | - |
dc.identifier.scopus | eid_2-s2.0-85144400820 | - |
dc.identifier.volume | 13658 LNCS | - |
dc.identifier.spage | 155 | - |
dc.identifier.epage | 174 | - |
dc.identifier.isi | WOS:000897034100008 | - |
dc.identifier.eisbn | 9783031210372 | - |