Nicolas Chappe

I am a post-doctoral researcher at Verimag, working on verified compilation.

Before that, I was a PhD student in the CASH team at LIP, ENS de Lyon.

You can find my CV here.

Research

My main research interests are compilers and programming languages, both from theoretical and practical points of view.

My latest draft is about a Rocq library of 12 simulation relations for verified compilation, with a novel mutually coinductive characterization of divergence sensitivity.

In the context of my PhD, I developed tools to reason about concurrent programs using monadic interpreters in the Rocq prover, with the distant long-term perspective of extending the Vellvm project to concurrent programs.

The main contributions of my PhD are as follows:

• I am a major contributor to the Choice Trees Rocq library, a coinductive data structure to represent and reason about nondeterministic programs. See its introductory paper (POPL'23), or the revised and extended version (accepted at JFP) for CTrees 2.0.
• I used the Choice Trees library to define a semantic model for a concurrent subset of LLVM IR in a CPP'25 paper.

My PhD thesis is available here, and the slides here.

Publications

• Nicolas Chappe, Paul He, Ludovic Henrio, Eleftherios Ioannidis, Yannick Zakowski and Steve Zdancewic. Choice Trees: Representing and Reasoning about Nondeterministic, Recursive, and Impure Programs in Rocq. Accepted for publication in the Journal of Functional Programming.
• Nicolas Chappe, Ludovic Henrio, Yannick Zakowski. Monadic Interpreters for Concurrent Memory Models: Executable semantics of a concurrent subset of LLVM IR.In Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '25), 283–298.
• Eddy Caron and Nicolas Chappe. FicWebBoard: A Playful and Collaborative Learning Platform Built for All People and All Programming Languages. 2023 IEEE ASEE Frontiers in Education Conference (FIE), Oct 2023
• Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski and Steve Zdancewic. Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. Proc. ACM Program. Lang. 7, POPL, Article 61 (January 2023), 31 pages.
• Nicolas Chappe, Ludovic Henrio, Amaury Maillé, Matthieu Moy and Hadrien Renaud. An Optimised Flow for Futures: from Theory to Practice. The Art, Science, and Engineering of Programming, vol. 6, no. 1, 2022, article 3.

Drafts

• The Sims: A Family of Simulations for Verified Compilation (Draft), Corresponding Rocq development

Teaching

In 2021-2022, I wrote a set of exercise sheets for the systems and networking labs of the then-new M2 préparation à l'agrégation of the CS department at ENS de Lyon. You can find them here (in French).

For further information on my teaching activities, see my CV.