A Dependent Type Theory for Meta-programming with Intensional Analysis

This conference talk from POPL 2025 introduces DeLaM, a dependent layered modal type theory that enables meta-programming in Martin-Löf type theory (MLTT) with recursion principles on open code. Explore a three-layered approach: static syntax objects without computation, pure MLTT with computational behaviors, and a meta-programming layer supporting code quotation, composition, analysis, and execution. Learn how DeLaM provides a dependently typed foundation for both type-safe code generation and code analysis, with proven weak normalization and decidability of convertibility using Kripke logical relations. Presented by Jason Z. S. Hu and Brigitte Pientka from McGill University at the ACM SIGPLAN POPL 2025 conference, this 20-minute presentation delves into advanced concepts including dependent types, logical relations, modal type theory, and contextual types.