Reynald Affeldt

57 papers B 13C 8Misc 1Journal 23Unranked 12
YearRankTypeTitle / Venue / Authors
2026 J jnl
A Foundation for Differentiable Logics using Dependent Type Theory.
CoRR
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark
2025 B conf
A Formal Foundation for Equational Reasoning on Probabilistic Programs.
APLAS
Reynald Affeldt, Yoshihiro Ishiguro, Zachary Stone
2025 J jnl
A practical formalization of monadic equational reasoning in dependent-type theory.
J. Funct. Program.
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2025 C conf
An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols.
FORTE
Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2025 B conf
Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation.
ITP
Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa
2025 — conf
Quantifiers for Differentiable Logics in Rocq (Extended Abstract).
SAIV
Jairo Miguel Marulanda-Giraldo, Ekaterina Komendantskaya, Alessandro Bruni, Reynald Affeldt, Matteo Capucci, Enrico Marchioni
2024 B conf
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq.
ITP
Reynald Affeldt, Zachary Stone
2024 J jnl
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq.
CoRR
Reynald Affeldt, Zachary Stone
2024 B conf
Robust Mean Estimation by All Means (Short Paper).
ITP
Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann
2024 B conf
Taming Differentiable Logics with Coq Formalisation.
ITP
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark
2024 J jnl
Taming Differentiable Logics with Coq Formalisation.
CoRR
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark
2023 J jnl
A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory.
CoRR
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2023 B conf
Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq.
APLAS
Ayumu Saito, Reynald Affeldt
2023 J jnl
Measure Construction by Extension in Dependent Type Theory with Application to Integration.
J. Autom. Reason.
Reynald Affeldt, Cyril Cohen
2023 B conf
Semantics of Probabilistic Programs using s-Finite Kernels in Coq.
CPP
Reynald Affeldt, Cyril Cohen, Ayumu Saito
2022 J jnl
Measure Construction by Extension in Dependent Type Theory with Application to Integration.
CoRR
Reynald Affeldt, Cyril Cohen
2022 B conf
Towards a Practical Library for Monadic Equational Reasoning in Coq.
MPC
Ayumu Saito, Reynald Affeldt
2021 J jnl
A trustful monad for axiomatic reasoning with probability and nondeterminism.
J. Funct. Program.
Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa
2020 J jnl
A Library for Formalization of Linear Error-Correcting Codes.
J. Autom. Reason.
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2020 J jnl
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism.
CoRR
Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa
2020 — conf
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis.
IJCAR (2)
Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
2020 — conf
Extending Equational Monadic Reasoning with Monad Transformers.
TYPES
Reynald Affeldt, David Nowak
2020 J jnl
Extending Equational Monadic Reasoning with Monad Transformers.
CoRR
Reynald Affeldt, David Nowak
2020 C conf
Formal Adventures in Convex and Conical Spaces.
CICM
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2020 J jnl
Formal Adventures in Convex and Conical Spaces.
CoRR
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2019 B conf
A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning.
MPC
Reynald Affeldt, David Nowak, Takafumi Saikawa
2019 B conf
Proving Tree Algorithms for Succinct Data Structures.
ITP
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka
2019 J jnl
Proving tree algorithms for succinct data structures.
CoRR
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka
2018 C conf
Examples of Formal Proofs about Data Compression.
ISITA
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2018 J jnl
Formalization Techniques for Asymptotic Reasoning in Classical Analysis.
J. Formaliz. Reason.
Reynald Affeldt, Cyril Cohen, Damien Rouhling
2018 J jnl
Safe Low-level Code Generation in Coq Using Monomorphization and Monadification.
J. Inf. Process.
Akira Tanaka, Reynald Affeldt, Jacques Garrigue
2017 B conf
Formal foundations of 3D geometry to model robot manipulators.
CPP
Reynald Affeldt, Cyril Cohen
2016 C conf
Formal Verification of the rank Algorithm for Succinct Data Structures.
ICFEM
Akira Tanaka, Reynald Affeldt, Jacques Garrigue
2016 C conf
Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes.
ISITA
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
2015 B conf
Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory.
ITP
Reynald Affeldt, Jacques Garrigue
2014 J jnl
An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing.
J. Formaliz. Reason.
Reynald Affeldt, Kazuhiko Sakaguchi
2014 J jnl
Formalization of Shannon's Theorems.
J. Autom. Reason.
Reynald Affeldt, Manabu Hagiwara, Jonas Sénizergues
2014 C conf
Formalization of the variable-length source coding theorem: Direct part.
ISITA
Ryosuke Obi, Manabu Hagiwara, Reynald Affeldt
2014 — conf
What could Coq do for Database Software? - A Progress Report.
JFLA
Yoichi Hirai, Reynald Affeldt
2013 J jnl
On construction of a library of formally verified low-level arithmetic functions.
Innov. Syst. Softw. Eng.
Reynald Affeldt
2013 — conf
Towards formal verification of TLS network packet processing written in C.
PLPV
Reynald Affeldt, Nicolas Marti
2012 J jnl
Certifying assembly with formal security proofs: The case of BBS.
Sci. Comput. Program.
Reynald Affeldt, David Nowak, Kiyoshi Yamada
2012 — conf
Formal network packet processing with minimal fuss: invertible syntax descriptions at work.
PLPV
Reynald Affeldt, David Nowak, Yutaka Oiwa
2012 B conf
Formalization of Shannon's Theorems in SSReflect-Coq.
ITP
Reynald Affeldt, Manabu Hagiwara
2012 Misc conf
On construction of a library of formally verified low-level arithmetic functions.
SAC
Reynald Affeldt
2009 J jnl
A Certified Verifier for a Fragment of Separation Logic.
Inf. Media Technol.
Nicolas Marti, Reynald Affeldt
2009 J jnl
Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Reynald Affeldt, David Nowak, Kiyoshi Yamada
2009 J jnl
Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS.
IACR Cryptol. ePrint Arch.
Reynald Affeldt, David Nowak, Kiyoshi Yamada
2009 — conf
Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables.
Formal to Practical Security
Reynald Affeldt, Hubert Comon-Lundh
2007 C conf
Formal Proof of Provable Security by Game-Playing in a Proof Assistant.
ProvSec
Reynald Affeldt, Miki Tanaka, Nicolas Marti
2006 — conf
An Approach to Formal Verification of Arithmetic Functions in Assembly.
ASIAN
Reynald Affeldt, Nicolas Marti
2006 C conf
Formal Verification of the Heap Manager of an Operating System Using Separation Logic.
ICFEM
Nicolas Marti, Reynald Affeldt, Akinori Yonezawa
2004 — conf
A Coq Library for Verification of Concurrent Programs.
LFM@IJCAR
Reynald Affeldt, Naoki Kobayashi
2004 J jnl
Les espaces d'interaction Vers une géométrie des systèmes d'agents mobiles.
Obj. Logiciel Base données Réseaux
Frédéric Peschanski, Reynald Affeldt, Jean-Pierre Briot
2004 — conf
Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes.
EXPRESS
Reynald Affeldt, Naoki Kobayashi
2002 — conf
Formalization and Verification of a Mail Server in Coq.
ISSS
Reynald Affeldt, Naoki Kobayashi
2002 — conf
Supporting objects in run-time bytecode specialization.
ASIA-PEPM
Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, Akinori Yonezawa