WG211/M7Weirich1
Adventures in Dependently-Typed Metatheory
Stephanie Weirich with Limin Jia, Jianzhou Zhao, Vilhelm Sj"oberg
Work-in-progress report
Dependent type systems allow users to include computations in types, thereby allowing arbitrary expression of program properties. Because types include computations, the type system of such language must include a definition of program equivalence. For example, the type checker might reduce computations to some normal form to determine if they are the same. However, there are many ways to define equivalence for programs, and if we change our mind about what sort of equivalence to use, we must do all of the metatheory of the dependently-typed language over. For example, some definitions of equivalence may choose to ignore computationally-irrelevant terms, others may or may not be decidable if the computation language includes non-termination.
In this talk, I will report on initial progress to define a language where the definition of equivalence is held abstract. Instead, we seek to determine the properties of the equivalence relation that are necessary to show that the language is type sound.
- 211-deptyp.pdf : Slides
