Good Friends are Hard to Find! - Thomas Brihaye; Nicolas Markey; Mohamed Ghannem; Lionel Rieg (TIME, 2008)

Extracting Herbrand trees in classical realizability using forcing. - Lionel Rieg (CSL, 2013)

Extracting Herbrand trees from Coq - Lionel Rieg (CoRR, 2013)

On Forcing and Classical Realizability. (Forcing et réalisabilité classique). - Lionel Rieg (2014)

A Certified Universal Gathering Algorithm for Oblivious Mobile Robots. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (CoRR, 2015)

Impossibility of gathering, a certification. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (Inf. Process. Lett., 2015)

Brief Announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (PODC, 2016)

Synchronous Gathering Without Multiplicity Detection: A Certified Algorithm. - Thibaut Balabonski; Amélie Delga; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (SSS, 2016)

Certified Universal Gathering in mathbb R ^2 for Oblivious Mobile Robots. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (DISC, 2016)

Certified Universal Gathering in $R^2$ for Oblivious Mobile Robots. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (CoRR, 2016)

Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems. - Thibaut Balabonski; Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (FMICS-AVoCS, 2017)

A formally verified compiler for Lustre. - Timothy Bourke; Lélio Brun; Pierre-Évariste Dagand; Xavier Leroy; Marc Pouzet; Lionel Rieg (PLDI, 2017)

A Foundational Framework for Certified Impossibility Results with Mobile Robots on Graphs. - Thibaut Balabonski; Robin Pelle; Lionel Rieg; Sébastien Tixeuil (ICDCN, 2018)

Brief Announcement Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. - Thibaut Balabonski; Pierre Courtieu; Robin Pelle; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (SSS, 2018)

Integrating Formal Schedulability Analysis into a Verified OS Kernel. - Xiaojie Guo 003; Maxime Lesourd; Mengqi Liu 001; Lionel Rieg; Zhong Shao 001 (CAV (2), 2019)

Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots. - Thibaut Balabonski; Pierre Courtieu; Robin Pelle; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (NETYS, 2019)

Dependent Pearl: Normalization by realizability. - Pierre-Évariste Dagand; Lionel Rieg; Gabriel Scherer (CoRR, 2019)

Towards Coq-verified Esterel Semantics and Compiling. - Gérard Berry; Lionel Rieg (CoRR, 2019)

Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. - Mengqi Liu 001; Lionel Rieg; Zhong Shao 001; Ronghui Gu; David Costanzo; Jung-Eun Kim; Man-Ki Yoon (Proc. ACM Program. Lang., 2020)

A generic approach for the certified schedulability analysis of software systems. - Xiaojie Guo 003; Lionel Rieg; Paolo Torrini (RTCSA, 2021)

Computer Aided Formal Design of Swarm Robotics Algorithms. - Thibaut Balabonski; Pierre Courtieu; Robin Pelle; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (SSS, 2021)

Swarms of Mobile Robots: Towards Versatility with Safety. - Pierre Courtieu; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (Leibniz Trans. Embed. Syst., 2022)

Revisiting Timing Anomalies in Predictable In-Order Pipelines. - Lilia Rouizi; Mihail Asavoae; Benjamin Binder 001; Lionel Rieg; Florian Brandner (ECRTS, 2025)

Deterministic Color-Optimal Self-stabilizing Semi-synchronous Gathering: A Certified Algorithm. - François Bonnet 001; Quentin Bramas; Pierre Courtieu; Xavier Défago; Lionel Rieg; Sébastien Tixeuil; Xavier Urbain (SIROCCO, 2025)

Towards a Coq-verified Chain of Esterel Semantics. - Lionel Rieg; Gérard Berry (Leibniz Trans. Embed. Syst., 2025)