A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract)

Meta-programming is the art of writing programs that produce or manipulate other programs. This allows programmers to automate error-prone or repetitive tasks, and exploit domain-specific knowledge to customize the generated code. Unfortunately, writing safe meta-programs remains very challenging, since errors in the generated code are usually only detected when running it, but not at the time when code is generated. How can we design a flexible and expressive meta-programming framework where we provide a range of safety guarantees about the code that is being generated and the code generator itself? We revisit Cocon, a type-theoretic framework for certified meta-programming. Cocon is a two-level type theory: at its base is the logical framework LF where we can represent domain-specific languages (DSL) ranging from simply-typed to polymorphic languages; on top sits a Martin-Loef type theory where we can write recursive programs and proofs about those DSLs using pattern matching. In particular, when the DSL is contained in Martin-Loef type theory we can use reflection and leverage MLTT's evaluation to execute programs written in a given DSL.Hence, we can derive type-safe meta-programming systems for a range of DSLs.