A Dependent Type Theory for Meta-programming with Intensional Analysis
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.
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 |