Rencontre, April 4, 2024
Programme
 10:30 – 12:00

Brigitte Pientka (McGill University)Invited talk: A Framework for Certified Metaprogramming
Metaprogramming is the art of writing programs that produce or manipulate other programs. This allows programmers to automate errorprone or repetitive tasks, and exploit domainspecific knowledge to customize the generated code. Hence, metaprogramming 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 metaprograms 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 metaprograms, 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 metaprogramming based on Cocon, a MartinLeof dependent type theory for defining logics and proofs that allows us to represent domainspecific 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 metaprogramming systems  from compiling metaprogramming with STLC or System F to compiling metaprogramming 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 welldefinedness of the composition of Proponent and Opponentstrategies. Indeed this crucial point involves a variant of the socalled infinite chattering problem, which we solve by looking into uniqueness properties of fixpoint equations in iterative monads.
 15:15 – 16:15

Christine Tasson (ISAESUPAERO)
Synchronous languages are now a standard industry tool for critical embedded systems. Designers write highlevel specifications by composing streams of values using block diagrams. These languages have been extended with Bayesian reasoning to program statespace 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 unnormalized density functions which maps random variable values to a result and positive score. The coiterative 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 statespace models with constant parameters.
This is joint work with Guillaume Baudart and Louis Mandel.