Dissertation
Elaborating inductive definitions in the calculus of dependent lambda eliminations
University of Iowa
Doctor of Philosophy (PhD), University of Iowa
Summer 2023
DOI: 10.25820/etd.006888
Abstract
In programming languages, algebraic datatypes along with the associated features of pattern matching and recursion provide notational convenience for problem-solving. This convenience helps programmers abstract away from low-level details and focus on the problem at hand, thereby helping them avoid software bugs. Because of this expressivity, however, high-level programming languages with these features are complex software artifacts, and their implementations may have subtle and undesirable interactions. For general-purpose languages these interactions may result in unintuitive edge cases, run-time crashes, unintended non-termination, or unexpected behavior. For programming languages that serve also as interactive theorem provers (ITPs), the consequences of bugs in such systems may be as dire as losing trust in proofs carried out within them.
While many lines of evidence can increase trust in software, such as testing, the most robust is formal, machine-checked verification. Unfortunately, formal verification of a fully-fledged programming language is a Herculean task. To facilitate this endeavor, language designers can turn to elaboration, a term of art describing the type-guided translation of a language into a simpler kernel language. Such a translation can then be proven correct, with the kernel language being easier to test or formally verify.
This dissertation concerns the elaboration of inductive datatypes into the calculus of dependent lambda eliminations (CDLE), a dependent type theory designed to be both expressive and tiny. Unlike other type theories, which must bring datatypes and their associated induction principles into the kernel language, in CDLE it is possible to derive datatypes and their induction principles from a relatively small set of language features. This dissertation demonstrates how higher-level syntax for many desirable features --- inductive datatype declarations, pattern matching, recursion and induction with a form of typed-based termination checking --- can be soundly translated into CDLE.
Details
- Title: Subtitle
- Elaborating inductive definitions in the calculus of dependent lambda eliminations
- Creators
- Christa Jenkins
- Contributors
- Aaron Stump (Advisor)Brandon Myers (Committee Member)C Tinelli (Committee Member)Garrett Morris (Committee Member)Omar Haider Chowdhury (Committee Member)
- Resource Type
- Dissertation
- Degree Awarded
- Doctor of Philosophy (PhD), University of Iowa
- Degree in
- Computer Science
- Date degree season
- Summer 2023
- Publisher
- University of Iowa
- DOI
- 10.25820/etd.006888
- Number of pages
- xiii, 300 pages
- Copyright
- Copyright 2023 Christa Jenkins
- Language
- English
- Date submitted
- 07/20/2023
- Description illustrations
- illustrations
- Description bibliographic
- Includes bibliographical references (pages 291-299) and index.
- Public Abstract (ETD)
Software is everywhere in modern life, to the extent that sometimes our lives depend upon it! But, how can we trust this software? Famously, computer scientist Edsger Dijkstra once said “Program testing can be used to show the presence of bugs, but never to show their absence!" Machine-checked verification offers the strongest guarantee that software is without bugs, and interactive theorem provers (ITPs) are a popular tool for this purpose. However, this then raises the question: who checks the checker? This is especially vexing as ITPs are themselves complicated pieces of software, with features being added to aid humans in verifying ever more complex software.
One of the ways to handle complexity like this is to translate it into simpler terms. Unlike the natural languages used by people, when dealing with programs and rigorous proof it is vital to ensure that no details are lost in translation. That is the focus of this dissertation: taking the near-ubiquitous feature of inductive definitions, which play a vital role in helping us write programs and reason about them while at the same time introducing complexity into the ITPs that implement them, and translating them in a meaning-preserving way into the much simpler theory of the Calculus of Dependent Lambda Eliminations.
- Academic Unit
- Computer Science
- Record Identifier
- 9984454186902771
Metrics
4 File views/ downloads
37 Record Views