A Dependent Type Theory for Meta-programming with Intensional Analysis
summary
Introduces DeLaM, a concrete dependent layered modal type theory that implements three layers (syntax, MLTT, meta) with quoting of open code, composition, recursion on code, pattern matching and execution of code objects as first-class terms. Uses a non‑cumulative Tarski universe hierarchy, a lifting lemma, reducibility candidates and Kripke logical relations to prove weak normalization and decidability of convertibility. Provides a syntactic typing judgment that separates which equations hold at each layer and a worked normalization proof.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:42Meta-programming in type theory
- 3:32Motivation
- 5:38Code generation examples
- 6:46Three-layered architecture
- 8:32Typing judgment
- 9:56Lifting lemma
- 11:19Contributions
- 12:42Meta-programming spectrum
- 13:50Q&A
related talks
50mA Type-Theoretic Framework for Certified Meta-programming
45mLogic Meta Programming for Functional Languages
53mIntroduction to Intuitionistic Type Theory
15mStaged Compilation with Two-Level Type Theory
19mExtensible Metatheory Mechanization via Family Polymorphism
52mType Theory and its Meaning Explanations
36mDependently Typed Multi-Stage Programming, Revisited
24mGeneralization of meta programs with dependent types in mtac2 with mtac2