On the design of a gradual dependently typed language for programming
department or school: Science, Faculty of
department or school: Computer Science, Department of
data provider: DSpace
degree campus: UBCV
creator: Eremondi, Joseph S.
issued: 2023-03-29T18:27:51Z
issued: 2023
related degree: Doctor of Philosophy - PhD
degree grantor: University of British Columbia
description: Dependently typed programming languages provide a way to write programs, specifications, and correctness proofs using a single language. If a dependent type checker accepts a program, the programmer can be assured that it behaves according to the specification given in its types. However, dependently typed programming languages can be hard to use. Gradual types provide a way to mix dynamically and statically typed code in a single language. Under this paradigm, programs may have imprecise types, causing certain type checks to be deferred to run time. We build the theoretical foundations for combining gradual and dependent types in a programming language, with the aim of making dependent types easier to use. The differences between these two paradigms lead to inherent tensions when choosing the properties such a language should satisfy. Gradual typing's effectful nature conflicts with the compile-time reductions of dependent type checking. Gradual run-time type comparisons clash with dependent types containing terms that bind variables. This dissertation identifies such tensions and proposes a design that finds balance between the conflicting goals. Our contribution has three parts: First, we present a foundational calculus for gradual dependent types, with functions, function types and universes. To ensure that type checking terminates, we reduce compile-time terms with approximate normalization, producing imprecise results when the available type information cannot guarantee termination. We use hereditary substitution to show that approximate normalization always terminates. Second, we present a notion of propositional equality for gradual dependent types. We devise a method of tracking run-time consistency information between imprecise equated terms, and introduce a composition operator in the language itself. Third, we show that the first and second contributions can be combined, giving a language with approximate normalization that supports inductive types and p…
aggregated CHO: https://circle.library.ubc.ca/rest/handle/2429/84109
note: One Design of a Gradual Dependently TypedLanguage for ProgrammingbyJoseph S. EremondiBSc. Honours Computer Science, University of Saskatchewan, 2014BSc. Mathematics, University of Saskatchewan, 2014MSc. Computing Science, Universiteit Utrecht, 2016a thesis submitted in partial fulfillmentof the reqirements for the degree ofDoctor of Philosophyinthe faculty of graduate and postdoctoral studies(Computer Science)e University of British Columbia(Vancouver)March 2023© Joseph S. Eremondi, 2023e following individuals certify that they have read, and recommend to theFaculty of Graduate and Postdoctoral Studies for acceptance, the thesis entitled:On eDesign of aGradualDependentlyTypedLanguage for Programmingsubmi ed by Joseph S. Eremondi in partial ful llment of the requirements forthe degree of Doctor of Philosophy in Computer Science.Examining Committee:Ronald Garcia, Associate Professor, Computer Science, UBCSupervisorWilliam Bowman, Assistant Professor, Computer Science, UBCSupervisory Commi ee MemberE´ric Tanter, Professor, Computer Science Department, University of ChileSupervisory Commi ee MemberIvan Beschastnikh, Associate Professor, Computer Science, UBCUniversity ExaminerSathish Gopalakrishnan, Associate Professor, Electrical and Computer Eng., UBCUniversity ExaminerDaniel Licata, Associate Professor, Computer Science, Wesleyan UniversityExternal ExamineriiAbstractDependently typed programming languages provide a way to write programs,specications, and correctness proofs using a single language. If a dependenttype checker accepts a program, the programmer can be assured that it behavesaccording to the speci cation given in its types. However, dependently typedprogramming languages can be hard to use.Gradual types provide a way to mix dynamically and statically typed codein a single language. Under this paradigm, programs may have imprecise types,causing certain type checks to be deferred to run time.We build the theoretical foundations for combining gradual and dep…
has type: Thesis/Dissertation
date issued: 2023-05
is shown at: 10.14288/1.0428823
language: eng
degree discipline: Computer Science
provider: Vancouver : University of British Columbia Library
publisher: University of British Columbia
rights: Attribution 4.0 International
rights URI: http://creativecommons.org/licenses/by/4.0/
scholar level: Graduate
contributor: Garcia, Ronald (Professor of computer science)
type: Text
identifier URI: http://hdl.handle.net/2429/84109