Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell University Graduate School
  3. Cornell Theses and Dissertations
  4. Efficient Runtimes for Gradual Typing

Efficient Runtimes for Gradual Typing

File(s)
Muehlboeck_cornellgrad_0058F_11751.pdf (2.37 MB)
integrated_subtyping_proofs.zip (1 MB)
Permanent Link(s)
https://doi.org/10.7298/k9ra-2795
https://hdl.handle.net/1813/70010
Collections
Cornell Theses and Dissertations
Author
Muehlboeck, Fabian
Abstract

This dissertation concerns the design and implementation of programming languages featuring gradual typing - which is the idea that some parts of a program may be type-checked dynamically while others are type-checked statically. This lets programmers trade off between the costs and benefits of using static type-checking for each individual part of their program as needed, and even eventually change their decisions about those trade-offs. Designing gradually typed languages has its own trade-offs: existing gradually typed languages had to essentially decide between being efficient versus behaving in expected and safe ways. Since many of those languages were just gradually typed variants of existing languages, those trade-offs were largely forced by the original language design. Here, we look at the design questions around gradual typing in an unconstrained scenario - what if we design a new language featuring gradual typing from the ground up? In particular, we explore these questions for nominal object-oriented programming languages. Designing a new language from the ground up lets us co-design the features of the language and its implementation. Accordingly, in this dissertation, we tackle a variety of design questions of particular importance to gradual typing, such as decidable subtyping, as well as questions of implementation, most importantly efficient casting techniques, which we evaluate using benchmarks from the literature on efficiency in gradual typing. The results presented here show that when gradual typing is co-designed with the rest of the type system and with an eye towards efficiency, it is possible to obtain both the desired formal properties proposed so far for gradual type systems and very low overheads due to gradual typing. This points the way towards a new generation of programming languages that can be used to seamlessly transition between personal scripting or rapid prototyping and large-scale software engineering.

Description
454 pages
Supplemental file(s) description: Mechanized Proofs for Chapter 3.
Date Issued
2019-12
Keywords
Decidability
•
Gradual Typing
•
Programming Language Design
•
Subtyping
•
Type Systems
Committee Chair
Tate, Ross Everett
Committee Member
Kozen, Dexter Campbell
Miller, Richard William
Degree Discipline
Computer Science
Degree Name
Ph. D., Computer Science
Degree Level
Doctor of Philosophy
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International
Rights URI
https://creativecommons.org/licenses/by-nc-nd/4.0/
Type
dissertation or thesis
Link(s) to Catalog Record
https://newcatalog.library.cornell.edu/catalog/13119659

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance