Formalization and Verification of a Mail Server in Coq. - Reynald Affeldt; Naoki Kobayashi 001 (ISSS, 2002)

Supporting objects in run-time bytecode specialization. - Reynald Affeldt; Hidehiko Masuhara; Eijiro Sumii; Akinori Yonezawa (ASIA-PEPM, 2002)

Les espaces d'interaction Vers une géométrie des systèmes d'agents mobiles. - Frédéric Peschanski; Reynald Affeldt; Jean-Pierre Briot (Obj. Logiciel Base données Réseaux, 2004)

Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes. - Reynald Affeldt; Naoki Kobayashi 001 (EXPRESS, 2004)

A Coq Library for Verification of Concurrent Programs. - Reynald Affeldt; Naoki Kobayashi 001 (LFM@IJCAR, 2004)

An Approach to Formal Verification of Arithmetic Functions in Assembly. - Reynald Affeldt; Nicolas Marti (ASIAN, 2006)

Formal Verification of the Heap Manager of an Operating System Using Separation Logic. - Nicolas Marti; Reynald Affeldt; Akinori Yonezawa (ICFEM, 2006)

Formal Proof of Provable Security by Game-Playing in a Proof Assistant. - Reynald Affeldt; Miki Tanaka; Nicolas Marti (ProvSec, 2007)

Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables. - Reynald Affeldt; Hubert Comon-Lundh (Formal to Practical Security, 2009)

Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. - Reynald Affeldt; David Nowak; Kiyoshi Yamada (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2009)

A Certified Verifier for a Fragment of Separation Logic. - Nicolas Marti; Reynald Affeldt (Inf. Media Technol., 2009)

Formalization of Shannon's Theorems in SSReflect-Coq. - Reynald Affeldt; Manabu Hagiwara (ITP, 2012)

Formal network packet processing with minimal fuss: invertible syntax descriptions at work. - Reynald Affeldt; David Nowak; Yutaka Oiwa (PLPV, 2012)

Certifying assembly with formal security proofs: The case of BBS. - Reynald Affeldt; David Nowak; Kiyoshi Yamada (Sci. Comput. Program., 2012)

Towards formal verification of TLS network packet processing written in C. - Reynald Affeldt; Nicolas Marti (PLPV, 2013)

On construction of a library of formally verified low-level arithmetic functions. - Reynald Affeldt (Innov. Syst. Softw. Eng., 2013)

Formalization of the variable-length source coding theorem: Direct part. - Ryosuke Obi; Manabu Hagiwara; Reynald Affeldt (ISITA, 2014)

What could Coq do for Database Software? - A Progress Report. - Yoichi Hirai; Reynald Affeldt (JFLA, 2014)

Formalization of Shannon's Theorems. - Reynald Affeldt; Manabu Hagiwara; Jonas Sénizergues (J. Autom. Reason., 2014)

An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing. - Reynald Affeldt; Kazuhiko Sakaguchi (J. Formaliz. Reason., 2014)

Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory. - Reynald Affeldt; Jacques Garrigue (ITP, 2015)

Formal Verification of the rank Algorithm for Succinct Data Structures. - Akira Tanaka; Reynald Affeldt; Jacques Garrigue (ICFEM, 2016)

Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (ISITA, 2016)

Formal foundations of 3D geometry to model robot manipulators. - Reynald Affeldt; Cyril Cohen (CPP, 2017)

Examples of Formal Proofs about Data Compression. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (ISITA, 2018)

Formalization Techniques for Asymptotic Reasoning in Classical Analysis. - Reynald Affeldt; Cyril Cohen; Damien Rouhling (J. Formaliz. Reason., 2018)

Safe Low-level Code Generation in Coq Using Monomorphization and Monadification. - Akira Tanaka; Reynald Affeldt; Jacques Garrigue (J. Inf. Process., 2018)

Proving Tree Algorithms for Succinct Data Structures. - Reynald Affeldt; Jacques Garrigue; Xuanrui Qi; Kazunari Tanaka (ITP, 2019)

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. - Reynald Affeldt; David Nowak; Takafumi Saikawa (MPC, 2019)

Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. - Reynald Affeldt; Cyril Cohen; Marie Kerjean; Assia Mahboubi; Damien Rouhling; Kazuhiko Sakaguchi (IJCAR (2), 2020)

Formal Adventures in Convex and Conical Spaces. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (CICM, 2020)

Extending Equational Monadic Reasoning with Monad Transformers. - Reynald Affeldt; David Nowak (TYPES, 2020)

A Library for Formalization of Linear Error-Correcting Codes. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (J. Autom. Reason., 2020)

A trustful monad for axiomatic reasoning with probability and nondeterminism. - Reynald Affeldt; Jacques Garrigue; David Nowak; Takafumi Saikawa (J. Funct. Program., 2021)

Towards a Practical Library for Monadic Equational Reasoning in Coq. - Ayumu Saito; Reynald Affeldt (MPC, 2022)

Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq. - Ayumu Saito; Reynald Affeldt (APLAS, 2023)

Semantics of Probabilistic Programs using s-Finite Kernels in Coq. - Reynald Affeldt; Cyril Cohen; Ayumu Saito (CPP, 2023)

Measure Construction by Extension in Dependent Type Theory with Application to Integration. - Reynald Affeldt; Cyril Cohen (J. Autom. Reason., 2023)

Robust Mean Estimation by All Means (Short Paper). - Reynald Affeldt; Clark W. Barrett; Alessandro Bruni; Ieva Daukantas; Harun Khan; Takafumi Saikawa; Carsten Schürmann (ITP, 2024)

Taming Differentiable Logics with Coq Formalisation. - Reynald Affeldt; Alessandro Bruni; Ekaterina Komendantskaya; Natalia Slusarz; Kathrin Stark (ITP, 2024)

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. - Reynald Affeldt; Zachary Stone (ITP, 2024)

Formalisation of Differentiable Logics in Coq. - Natalia Slusarz; Reynald Affeldt; Alessandro Bruni (DROPS Artifacts, 2024)

An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols. - Cheng-Hui Weng; Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (FORTE, 2025)

A practical formalization of monadic equational reasoning in dependent-type theory. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (J. Funct. Program., 2025)