Campus Event Calendar
Event Entry
What and Who
Cocon: A Type-Theoretic Framework for Certified Meta-programming
Brigitte Pientka
McGill University
SWS Colloquium
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 15 December 2023
09:00
60 Minutes
E1 5
029
Saarbrücken
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. Hence, meta-programming is widely used in a range of technologies: from cryptographic message authentication in secure network protocols to supporting reflection in proof environments such as Lean or Coq.
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 revisits Cocon, a Martin-Loef dependent type theory for defining logics and proofs, as a framework for certified meta-programming. Cocon allows us to represent domain-specific languages (DSL) within the logical framework LF and in addition write recursive meta-programs and proofs about those DSLs. In particular, we can embed into LF STLC or System F, or even MLTT itself and then write programs about those encodings using Cocon itself. This means Cocon can be viewed as a type-theoretic framework for certified meta-programming.
This work revisits the LICS'19 paper "A Type Theory for Defining Logics” by Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini and reframes it as a foundation for meta-programming. It highlights what is necessary to use Cocon as a type-theoretic foundation for certified meta-programming and how to build such a certified meta-programming system from the ground up.
This is joint work with Jason Z. Hu and Junyoung Jang.
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 revisits Cocon, a Martin-Loef dependent type theory for defining logics and proofs, as a framework for certified meta-programming. Cocon allows us to represent domain-specific languages (DSL) within the logical framework LF and in addition write recursive meta-programs and proofs about those DSLs. In particular, we can embed into LF STLC or System F, or even MLTT itself and then write programs about those encodings using Cocon itself. This means Cocon can be viewed as a type-theoretic framework for certified meta-programming.
This work revisits the LICS'19 paper "A Type Theory for Defining Logics” by Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rébecca Zucchini and reframes it as a foundation for meta-programming. It highlights what is necessary to use Cocon as a type-theoretic foundation for certified meta-programming and how to build such a certified meta-programming system from the ground up.
This is joint work with Jason Z. Hu and Junyoung Jang.
---
Please contact the Office team for Zoom link information.
Contact
Annika Meiser
+49 681 9303 9105
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
111
passcode not visible
logged in users only
Annika Meiser, 12/14/2023 09:15 -- Created document.