Rencontre, 4 avril 2024
Programme
- 10:30 – 12:00
-
Brigitte Pientka (McGill University)Invited talk: A Framework for Certified Meta-programming
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.
- 13:45 – 14:45
-
Peio Borthelle (Université Savoie Mont Blanc)Invited talk: Operational Game Semantics, certified in Coq
Operational game semantics (OGS) is a method for interpreting programs as strategies in suitable games, or more precisely as labelled transition systems over suitable games, in the sense of Levy and Staton. Such an interpretation is called sound when, for any two given programs, bisimilarity of associated strategies entails contextual equivalence. OGS has been applied to a variety of languages, with rather tedious soundness proofs. Concretely they transform a reduction relation into a full blown model interpreting open terms as a strategy for interacting with all possible execution environments. We have developed a Coq formalization of this construction, abstracting away some syntactic details of the considered language and keeping the computational content intact.
I will start this talk by motivating and presenting OGS intuitively, and will then give an overview of our contributions. Finally I will detail a technical point of the soundness proof, namely well-definedness of the composition of Proponent- and Opponent-strategies. Indeed this crucial point involves a variant of the so-called infinite chattering problem, which we solve by looking into uniqueness properties of fixpoint equations in iterative monads.
- 15:15 – 16:15
-
Christine Tasson (ISAE-SUPAERO)
Synchronous languages are now a standard industry tool for critical embedded systems. Designers write high-level specifications by composing streams of values using block diagrams. These languages have been extended with Bayesian reasoning to program state-space models which compute a stream of distributions given a stream of observations. However, the semantics of probabilistic models is only defined for scheduled equations -- a significant limitation compared to dataflow synchronous languages and block diagrams which do not require any ordering.
In this paper we propose two schedule agnostic semantics for a probabilistic synchronous language. The key idea is to interpret probabilistic expressions as a stream of un-normalized density functions which maps random variable values to a result and positive score. The co-iterative semantics interprets programs as state machines and equations are computed using a fixpoint operator. The relational semantics directly manipulates streams and is thus a better fit to reason about program equivalence. We use the relational semantics to prove the correctness of a program transformation required to run an optimized inference algorithm for state-space models with constant parameters.
This is joint work with Guillaume Baudart and Louis Mandel.
