A Type System With Containers
| dc.contributor.author | Thode, Michael | |
| dc.date.accessioned | 2021-10-04T14:29:23Z | |
| dc.date.available | 2021-10-04T14:29:23Z | |
| dc.date.issued | 2021-10-04 | |
| dc.date.submitted | 2021-09-23 | |
| dc.description.abstract | In this thesis, we will introduce the concept of containers as they apply to programming languages. Encapsulation is a common topic in programming languages with well understood benefits. Here, we will investigate its converse, namely containment. This includes a demonstration of how containers can be integrated into a programming language and what benefits they can bring. To support containment, a dependent type system is developed to enforce container rules. We add the notion of a container label to our types to indicate the container of the referred object. Around this type system we develop a language enhanced with container syntax. We use this language to show how containers can enable pass-by-value semantics, copying of complex objects and object serialization. An interpreter is implemented for this language to demonstrate its capabilities. Included is a container inferencing algorithm intended to minimize the extra syntax needed for container specification. A second formal system is also defined. This includes type rules, operational semantics and a proof of soundness. We show that correctly-typed programs will obey all container restrictions at run-time. We fully type the configuration used by the semantics; this includes concrete containers as run-time constructs which allow us to verify correct containment. Mappings are maintained from the container labels of the language to physical run-time containers. We show that as container labels are translated across scopes (e.g. a function call), the physical containers remain consistent. We conclude with a discussion on ways this system can be enhanced in the future to make containers easier to use, as well as describe additional capabilities such as version control of objects. | en |
| dc.identifier.uri | http://hdl.handle.net/10012/17616 | |
| dc.language.iso | en | en |
| dc.pending | false | |
| dc.publisher | University of Waterloo | en |
| dc.relation.uri | https://git.uwaterloo.ca/mthode/woven-c | en |
| dc.subject | programming languages | en |
| dc.subject | dependent types | en |
| dc.subject | ownership types | en |
| dc.subject | containers | en |
| dc.title | A Type System With Containers | en |
| dc.type | Master Thesis | en |
| uws-etd.degree | Master of Mathematics | en |
| uws-etd.degree.department | David R. Cheriton School of Computer Science | en |
| uws-etd.degree.discipline | Computer Science | en |
| uws-etd.degree.grantor | University of Waterloo | en |
| uws-etd.embargo.terms | 0 | en |
| uws.contributor.advisor | Lhotak, Ondrej | |
| uws.contributor.affiliation1 | Faculty of Mathematics | en |
| uws.peerReviewStatus | Unreviewed | en |
| uws.published.city | Waterloo | en |
| uws.published.country | Canada | en |
| uws.published.province | Ontario | en |
| uws.scholarLevel | Graduate | en |
| uws.typeOfResource | Text | en |