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 and sometimes frustrating, as traditionally errors in the generated code are only detected when running it, but not at the time when code is generated. To make it easier to write and maintain meta-programs, tools that allow us to detect errors during code generation – instead of when running the generated code – are essential. 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 framework for certified meta-programming. Cocon is a Martin-Löf dependent type theory for defining logics and proofs that allows us to represent domain-specific languages (DSL) within the logical framework LF and in addition write recursive programs and proofs about those DSLs using pattern matching. It is a two-level type theory where Martin-Löf type theory sits on top of the logical framework LF and supports a recursor over (contextual) LF objects. As a consequence, we can embed into LF STLC or System F, etc. and then write programs about those encodingsusing Cocon itself. This means Cocon can serve as a target for compiling meta-programming systems –from compiling meta-programming with STLC to System F. Moreover, Cocon supports writing an evaluator for each of these sub-languages. This also allows us to reflect back our encoded sub-language and evaluate their encodings using Cocon’s evaluation strategy.

I will conclude with highlighting more recent research directions and challenges hat build on the core ideas of Cocon and aim to support meta-programming and intensional code analysis directly in System F and Martin-Löf type theory.