I am a starting researcher in the πr² Inria team, hosted at the IRIF, Institut de Recherche en Informatique Fondamentale laboratory of the CNRS and Université de Paris. My research background is in mechanically-verified functional and logic programming. These days my main project is the Coq proof assistant, which I mainly use in conjunction with the Mathematical Components Library. Have a look at my publications and GitHub profile for recent projects; some recent topics are:

• jsCoq and SerAPI: New Interfaces for Theorem Proving ❲full proposal❳
• User Interfaces in Theorem Proving: We have develop jsCoq a new accesible interface for the Coq Proof Assistant. SerAPI is an experimental Coq toplevel intended to power the next-generation theorem proving IDEs.
• Formalized Computing in Relation Algebra: We study relational and categorical formalisms for constraint logic programming, lessening the gap between the operational and denotational models using combinatorial proof search, and provide mechanically verified implementations.
• Verification of Mechanism Design and Differential Privacy: We work on language-based tools to facilitate the construction of formally-verified mechanisms and real-world privacy.
• Programming Languages for Audio: Faust (Functional Audio Stream) is a functional programming language specifically designed for real-time signal processing and synthesis. We are working on logics for the verification of Faust programs, semantics, efficient compilation and extensions. See also the ANR FEEVER project.

I am a big fan of collaborative development platforms and I am often around on Gitter, Gitlab, and Github.

In the past I’ve worked on: logic programming, constraint solving, operating systems, server and network administration, collaborative web tools design and implementation, multi-paradigm declarative programming.