Final Exam - A Proof Theoretic Redesign of the Calculus of Dependent Lambda Eliminations

PhD Candidate: Andrew Marmaduke


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 expressiveness 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.

Advisor: Aaron Stump

Please contact Andrew Marmaduke for further details, if you wish to join his exam.

Tuesday, June 11, 2024 2:00pm
Virtual Event
View on Event Calendar
Individuals with disabilities are encouraged to attend all University of Iowa–sponsored events. If you are a person with a disability who requires a reasonable accommodation in order to participate in this program, please contact Tina Kimbrell in advance at 319-335-0713 or