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. Hence, meta-programming is widely used in a range of technologies: % from %generating optimized code for matrix computations in machine learning from cryptographic message authentication in secure network protocols to supporting reflection in proof environments such as Lean.

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.

This talk presents a framework for certified meta-programming based on Cocon, a Martin-Leof dependent type theory for defining logics and proofs that allows us to represent domain-specific languages (DSL) within the logical framework LF. In addition, Cocon allows us write recursive programs and proofs about those DSLs. We show how to embed into LF STLC or System F, etc. and then write programs about those encodings using Cocon itself. More importantly, we extend Cocon with the ability to reflect STLC terms defined in LF back into Cocon which allows us to execute and run those objects. This establishes Cocon as a target for compiling meta-programming systems -- from compiling meta-programming with STLC or System F to compiling meta-programming in CoC.