Reynald Affeldt

According to our database, Reynald Affeldt authored at least 42 papers between 2002 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq.

Reynald Affeldt, Zachary Stone

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Taming Differentiable Logics with Coq Formalisation.

Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Robust Mean Estimation by All Means (Short Paper).

Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2023

Measure Construction by Extension in Dependent Type Theory with Application to Integration.

Reynald Affeldt, Cyril Cohen

J. Autom. Reason., September, 2023

A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

CoRR, 2023

Semantics of Probabilistic Programs using s-Finite Kernels in Coq.

Reynald Affeldt, Cyril Cohen, Ayumu Saito

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq.

Ayumu Saito, Reynald Affeldt

Proceedings of the Programming Languages and Systems - 21st Asian Symposium, 2023

2022

Towards a Practical Library for Monadic Equational Reasoning in Coq.

Ayumu Saito, Reynald Affeldt

Proceedings of the Mathematics of Program Construction - 14th International Conference, 2022

2021

A trustful monad for axiomatic reasoning with probability and nondeterminism.

Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa

J. Funct. Program., 2021

2020

A Library for Formalization of Linear Error-Correcting Codes.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

J. Autom. Reason., 2020

Extending Equational Monadic Reasoning with Monad Transformers.

Reynald Affeldt, David Nowak

Proceedings of the 26th International Conference on Types for Proofs and Programs, 2020

Formal Adventures in Convex and Conical Spaces.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

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

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning.

Reynald Affeldt, David Nowak, Takafumi Saikawa

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

Proving Tree Algorithms for Succinct Data Structures.

Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

Safe Low-level Code Generation in Coq Using Monomorphization and Monadification.

Akira Tanaka, Reynald Affeldt, Jacques Garrigue

J. Inf. Process., 2018

Formalization Techniques for Asymptotic Reasoning in Classical Analysis.

Reynald Affeldt, Cyril Cohen, Damien Rouhling

J. Formaliz. Reason., 2018

Examples of Formal Proofs about Data Compression.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

Proceedings of the International Symposium on Information Theory and Its Applications, 2018

2017

Formal foundations of 3D geometry to model robot manipulators.

Reynald Affeldt, Cyril Cohen

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes.

Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

Proceedings of the 2016 International Symposium on Information Theory and Its Applications, 2016

Formal Verification of the rank Algorithm for Succinct Data Structures.

Akira Tanaka, Reynald Affeldt, Jacques Garrigue

Proceedings of the Formal Methods and Software Engineering, 2016

2015

Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory.

Reynald Affeldt, Jacques Garrigue

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

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 Shannon's Theorems.

Reynald Affeldt, Manabu Hagiwara, Jonas Sénizergues

J. Autom. Reason., 2014

What could Coq do for Database Software? - A Progress Report.

Yoichi Hirai, Reynald Affeldt

Proceedings of the 25. Journées francophones des langages applicatifs, 2014

Formalization of the variable-length source coding theorem: Direct part.

Ryosuke Obi, Manabu Hagiwara, Reynald Affeldt

Proceedings of the International Symposium on Information Theory and its Applications, 2014

2013

On construction of a library of formally verified low-level arithmetic functions.

Reynald Affeldt

Innov. Syst. Softw. Eng., 2013

Towards formal verification of TLS network packet processing written in C.

Reynald Affeldt, Nicolas Marti

Proceedings of the 7th Workshop on Programming languages meets program verification, 2013

2012

Certifying assembly with formal security proofs: The case of BBS.

Reynald Affeldt, David Nowak, Kiyoshi Yamada

Sci. Comput. Program., 2012

Formal network packet processing with minimal fuss: invertible syntax descriptions at work.

Reynald Affeldt, David Nowak, Yutaka Oiwa

Proceedings of the sixth workshop on Programming Languages meets Program Verification, 2012

Formalization of Shannon's Theorems in SSReflect-Coq.

Reynald Affeldt, Manabu Hagiwara

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2009

A Certified Verifier for a Fragment of Separation Logic.

Nicolas Marti, Reynald Affeldt

Inf. Media Technol., 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

Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables.

Reynald Affeldt, Hubert Comon-Lundh

Proceedings of the Formal to Practical Security, 2009

2007

Formal Proof of Provable Security by Game-Playing in a Proof Assistant.

Reynald Affeldt, Miki Tanaka, Nicolas Marti

Proceedings of the Provable Security, 2007

2006

Formal Verification of the Heap Manager of an Operating System Using Separation Logic.

Nicolas Marti, Reynald Affeldt, Akinori Yonezawa

Proceedings of the Formal Methods and Software Engineering, 2006

An Approach to Formal Verification of Arithmetic Functions in Assembly.

Reynald Affeldt, Nicolas Marti

Proceedings of the Advances in Computer Science, 2006

2004

A Coq Library for Verification of Concurrent Programs.

Reynald Affeldt, Naoki Kobayashi

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, 2004

Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes.

Reynald Affeldt, Naoki Kobayashi

Proceedings of the 11th International Workshop on Expressiveness in Concurrency, 2004

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

2002

Supporting objects in run-time bytecode specialization.

Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, Akinori Yonezawa

Proceedings of the ACM SIGPLAN ASIA-PEPM 2002, 2002

Formalization and Verification of a Mail Server in Coq.

Reynald Affeldt, Naoki Kobayashi

Proceedings of the Software Security -- Theories and Systems, 2002