8 citations · 14 across the 9 of their papers we have counts for
10 papers
Formal verification of tilt estimation using the Rocq prover
Reynald Affeldt, Lynda Bentoucha, Yoshihiro Ishiguro +1
The safe operation of a humanoid robot critically relies on accurate estimation of its vertical orientation, or ``tilt''. This requires a variety of mathematical tools, including t…
A Foundation for Differentiable Logics using Dependent Type Theory
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya +2
Differentiable logics are a family of quantitative logics originated in the machine learning literature. Because of their origin, differentiable logics often come equipped with ana…
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
Reynald Affeldt, Zachary Stone
Formalization of real analysis offers a chance to rebuild traditional proofs of important theorems as unambiguous theories that can be interactively explored. This paper provides a…
Taming Differentiable Logics with Coq Formalisation
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya +2
For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among…
A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful prog…
Measure Construction by Extension in Dependent Type Theory with Application to Integration
Reynald Affeldt, Cyril Cohen
We report on an original formalization of measure and integration theory in the Coq proof assistant. We build the Lebesgue measure following a standard construction that had not ye…
Extending Equational Monadic Reasoning with Monad Transformers
Reynald Affeldt, David Nowak
There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a st…
Formal Adventures in Convex and Conical Spaces
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
Convex sets appear in various mathematical theories, and are used to define notions such as convex functions and hulls. As an abstraction from the usual definition of convex sets i…
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
Reynald Affeldt, Jacques Garrigue, David Nowak +1
The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formaliz…
Proving tree algorithms for succinct data structures
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi +1
Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely one cleverly designed data representations and alg…