Dissertation
A proof theoretic redesign of the calculus of dependent Lambda eliminations
University of Iowa
Doctor of Philosophy (PhD), University of Iowa
Summer 2024
DOI: 10.25820/etd.007633
Abstract
Cedille is a dependently typed programming language with a significant history of encodeable features. All of this originating from a small type theory that extends the Calculus of Constructions with just three new features: erased function spaces, dependent intersections, and untyped equality. However, the last extension, untyped equality, is a source of undecidability. Perhaps worse from the perspective of modern type theory research, the untyped nature of equality is responsible for refuting function extensionality. This work attempts to refine the system of Cedille by specifically modifying the equality type into a new system: ç2. A philosophy borrowed from proof theory is applied to the design of Cedille, where equality is modelled after a standard identity type. This philosophy and design result in a partial success: a notion of proof reduction is strongly normalizing and supports all expected properties. Moreover, the system ç2 is shown to be consistent by a syntactic translation into the Calculus of Dependent Lambda Eliminations, the core type theory of Cedille.
Unfortunately, object reduction, a critical component of ç2 required for deciding conversion, is not strongly normalizing. Caused by the cast rule, casts are the last bastion of undecidability within the type theory. Thus, with the cast rule removed, the system ç2 is a proof theory in the spirit of Kreisel and Gentzen. The cast rule is, however, critical to the expressiveness of Cedille. Its benefits outweigh the costs. Thus, an external condition delineating when casts admit strong object normalization is described. Therefore, the full type theory ç2 is a proof theory relative to an oracle deciding this condition.
Details
- Title: Subtitle
- A proof theoretic redesign of the calculus of dependent Lambda eliminations
- Creators
- Andrew Marmaduke
- Contributors
- Aaron Stump (Advisor)Cesare Tinelli (Committee Member)J. Garrett Morris (Committee Member)William J. Bowman (Committee Member)
- Resource Type
- Dissertation
- Degree Awarded
- Doctor of Philosophy (PhD), University of Iowa
- Degree in
- Computer Science
- Date degree season
- Summer 2024
- Publisher
- University of Iowa
- DOI
- 10.25820/etd.007633
- Number of pages
- vii, 107 pages
- Copyright
- Copyright 2024 Andrew Marmaduke
- Language
- English
- Date submitted
- 06/25/2024
- Description bibliographic
- Includes bibliographical references (pages 101-107).
- Public Abstract (ETD)
- Language is a medium of expression, both artistic and technical. Like constrained art, a programming language consists of self-imposed technical restrictions. These restrictions yield interesting properties and enable a precise communication of ideas. The programming language Cedille is significantly constrained but with a small grammar and vocabulary that surpasses the expressive- ness of similar languages. This work proposes a refinement to Cedille that imposes more constraints to obtain better properties without sacrificing expressiveness. Precisely, Cedille’s notion of equality is modified and, as a result, several useful properties are proven about the refinement. Most importantly, however, is that almost all the communicable ideas in Cedille are not lost as a consequence.
- Academic Unit
- Computer Science
- Record Identifier
- 9984697941302771
Metrics
3 Record Views