A Dependent Type Theory for Meta-programming with Intensional Analysis
This program is tentative and subject to change.
In this paper, we introduce DeLaM, a dependent layered modal type theory which enables meta-programming in Martin-Löf type theory (MLTT) with recursion principles on open code. DeLaM includes three layers: the layer of static syntax objects of MLTT without any computation; the layer of pure MLTT with the computational behaviors; the meta-programming layer extends MLTT with support for quoting an open MLTT code object and composing and analyzing open code using recursion. We can also execute a code object at the meta-programming layer. The expressive power strictly increases as we move up in a given layer. In particular, while code objects only describe static syntax, we allow computation at the MLTT and meta-programming layer. As a result, DeLaM provides a dependently typed foundation for meta-programming that supports both type-safe code generation and code analysis. We prove the weak normalization of DeLaM and the decidability of convertibility using Kripke logical relations.
This program is tentative and subject to change.
Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change
15:00 - 16:20 | |||
15:00 20mTalk | A Dependent Type Theory for Meta-programming with Intensional Analysis POPL | ||
15:20 20mTalk | Avoiding signature avoidance in ML modules with zippers POPL | ||
15:40 20mTalk | Bidirectional Higher-Rank Polymorphism with Intersection and Union Types POPL | ||
16:00 20mTalk | Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs POPL |