- Audiences
- Interests
- Keywords
- Types
Final Exam - A Proof Theoretic Redesign of the Calculus of Dependent Lambda Eliminations
PhD Candidate: Andrew Marmaduke
Abstract
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