File Download
Supplementary
-
Citations:
- Appears in Collections:
postgraduate thesis: Applicative intersection types
Title | Applicative intersection types |
---|---|
Authors | |
Advisors | Advisor(s):Dos Santos Oliveira, BC |
Issue Date | 2023 |
Publisher | The University of Hong Kong (Pokfulam, Hong Kong) |
Citation | Xue, X. [薛旭]. (2023). Applicative intersection types. (Thesis). University of Hong Kong, Pokfulam, Hong Kong SAR. |
Abstract | A new programming language is often elaborated by introducing different features. Some of those features are not orthogonal, and their combination risks breaking the safety of the whole system, especially in statically typed languages. Also, the newly coming feature is conventionally reasoned in isolation or in a rather minimised calculus. It is not surprising for language researchers and implementers to desire a general framework that contains features as much as possible and has salient extensibility. Intersection types are a nice fit for this purpose.
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. Nevertheless, no previous calculus supports all those features at once.
In this thesis, 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 semantics 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 applicative dispatching relation that is used for the dynamic semantics. The two calculi and their proofs are formalised in the Coq theorem prover and we have a prototype implementation as well. |
Degree | Master of Philosophy |
Subject | Programming languages (Electronic computers) |
Dept/Program | Computer Science |
Persistent Identifier | http://hdl.handle.net/10722/327624 |
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Dos Santos Oliveira, BC | - |
dc.contributor.author | Xue, Xu | - |
dc.contributor.author | 薛旭 | - |
dc.date.accessioned | 2023-04-04T03:02:41Z | - |
dc.date.available | 2023-04-04T03:02:41Z | - |
dc.date.issued | 2023 | - |
dc.identifier.citation | Xue, X. [薛旭]. (2023). Applicative intersection types. (Thesis). University of Hong Kong, Pokfulam, Hong Kong SAR. | - |
dc.identifier.uri | http://hdl.handle.net/10722/327624 | - |
dc.description.abstract | A new programming language is often elaborated by introducing different features. Some of those features are not orthogonal, and their combination risks breaking the safety of the whole system, especially in statically typed languages. Also, the newly coming feature is conventionally reasoned in isolation or in a rather minimised calculus. It is not surprising for language researchers and implementers to desire a general framework that contains features as much as possible and has salient extensibility. Intersection types are a nice fit for this purpose. 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. Nevertheless, no previous calculus supports all those features at once. In this thesis, 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 semantics 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 applicative dispatching relation that is used for the dynamic semantics. The two calculi and their proofs are formalised in the Coq theorem prover and we have a prototype implementation as well. | - |
dc.language | eng | - |
dc.publisher | The University of Hong Kong (Pokfulam, Hong Kong) | - |
dc.relation.ispartof | HKU Theses Online (HKUTO) | - |
dc.rights | The author retains all proprietary rights, (such as patent rights) and the right to use in future works. | - |
dc.rights | This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. | - |
dc.subject.lcsh | Programming languages (Electronic computers) | - |
dc.title | Applicative intersection types | - |
dc.type | PG_Thesis | - |
dc.description.thesisname | Master of Philosophy | - |
dc.description.thesislevel | Master | - |
dc.description.thesisdiscipline | Computer Science | - |
dc.description.nature | published_or_final_version | - |
dc.date.hkucongregation | 2023 | - |
dc.identifier.mmsid | 991044657075003414 | - |