A Type-Theoretic Framework for Certified Meta-programming
summary
Claims a two-level type theory where LF encodes object languages and Martin-Löf type theory runs meta-programs, so generated code is typed and manipulable. Implements LF for code, MLTT for meta with pattern matching on open code, reflection and definable eval for languages that embed in MLTT. Proves normalization and consistency by mechanized logical relations, and extracts a verified type-checking kernel from the formal development; several example embeddings (STLC, System F) validate the design.
AI-written summary · about
chapters (20)
- 0:00Certified meta-programming intro
- 1:02Motivation for type-theoretic meta
- 2:25Meta-programming operations goals
- 7:02Untyped meta-programming limits
- 9:33Type theory for meta-programming
- 10:57Modal logic and box modality
- 12:43Typed code generation examples
- 15:36Box modalities strands
- 18:49Code and program separation
- 21:42Collapsing stages in modal TT
- 23:50Extending Martin-Löf TT
- 24:53Higher-order abstract syntax in LF
- 29:27Contextual types pattern matching
- 33:23COK type theory framework
- 35:32Evaluating code without eval
- 37:37Embedding System F
- 39:47Correct-by-construction kernel
- 41:33Meta-programming extensions
- 43:38Lessons and future work
- 45:07Q&A
related talks
45mLogic Meta Programming for Functional Languages
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
15mStaged Compilation with Two-Level Type Theory
01h 05mAll the Languages Together
19mExtensible Metatheory Mechanization via Family Polymorphism
22mMoebius: Metaprogramming using Contextual Types
23mType-Level Programming with Match Types