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

Jun 11, 2024

02:00 PM

Save to My Events

Virtual Event

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.

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 in advance at