arXiv subjects

Reynald Affeldt

Publications and source records attributed to Reynald Affeldt.

9 recordsLinked to original sources

arXiv2026

A Foundation for Differentiable Logics using Dependent Type Theory

Differentiable logics are a family of quantitative logics originated in the machine learning literature. Because of their origin, differentiable logics often come equipped with analytic properties that guarantee that they are differentiable. However, they usually lack an accompanying theory that describes their algebraic and proof-theoretic properties. Meanwhile, fuzzy logics, seen as substructural logics, have been studied algebraically and proof-theoretically, and some fuzzy logics with desirable analytic properties have also been used in machine learning. Our aim is to systematically compare analytic, algebraic and proof-theoretical properties of both fuzzy and differentiable logics. To this end, we formalize differentiable and fuzzy logics in a unified framework, encoded using the Mathcomp library in the Rocq proof assistant. We propose a single language specification to encompass multiple logics, using intrinsic typing to only allow valid and well-typed formulas for each of the logics that we encode: Yager, {\L}ukasiewicz, G\"{o}del and product fuzzy logics, as well as the differentiable logics DL2 and STL. Algebraically, we show how these logics can be interpreted using residuated lattices, which are prevalent in the theory of substructural logics. Analytically, we formalise the existence of a positive derivative for certain logical connectives, and to this end we formalise L'H\^opital's, contributing it to the Mathcomp library. Proof-theoretically, we formalise established sequent calculi for fuzzy logics, and we propose new sequent calculi for DL2 and STL$_{\infty}$, and formalise their soundness in our framework.

cs.LO↗

arXiv2024

Taming Differentiable Logics with Coq Formalisation

For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among these methods, differentiable logics (DLs) are used to translate propositional or first-order formulae into loss functions deployed for optimisation in machine learning. At the same time, recent attempts to give programming language support for verification of neural networks showed that DLs can be used to compile verification properties to machine-learning backends. This situation is calling for stronger guarantees about the soundness of such compilers, the soundness and compositionality of DLs, and the differentiability and performance of the resulting loss functions. In this paper, we propose an approach to formalise existing DLs using the Mathematical Components library in the Coq proof assistant. Thanks to this formalisation, we are able to give uniform semantics to otherwise disparate DLs, give formal proofs to existing informal arguments, find errors in previous work, and provide formal proofs to missing conjectured properties. This work is meant as a stepping stone for the development of programming language support for verification of machine learning.

cs.LO↗

arXiv2024

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq

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 comprehensive overview of the Lebesgue Differentiation Theorem formalized in the Coq proof assistant, from which the first Fundamental Theorem of Calculus (FTC) for the Lebesgue integral is obtained as a corollary. Proving the first FTC in this way has the advantage of decomposing into loosely-coupled theories of moderate size and of independent interest that lend themselves well to incremental and collaborative development. We explain how we formalize all the topological constructs and all the standard lemmas needed to eventually relate the definitions of derivability and of Lebesgue integration of MathComp-Analysis, a formalization of analysis developed on top of the Mathematical Components library. In the course of this experiment, we substantially enrich MathComp-Analysis and even devise a new proof for Urysohn's lemma.

cs.LO↗

arXiv2023

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

One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly because it is difficult to maintain pencil-and-paper proofs of large examples. We propose a formalization of a hierarchy of effects using monads in the Coq proof assistant that makes monadic equational reasoning practical. Our main idea is to formalize the hierarchy of effects and algebraic laws as interfaces like it is done when formalizing hierarchy of algebras in dependent type theory. Thanks to this approach, we clearly separate equational laws from models. We can then take advantage of the sophisticated rewriting capabilities of Coq and build libraries of lemmas to achieve concise proofs of programs. We can also use the resulting framework to leverage on Coq's mathematical theories and formalize models of monads. In this article, we explain how we formalize a rich hierarchy of effects (nondeterminism, state, probability, etc.), how we mechanize examples of monadic equational reasoning from the literature, and how we apply our framework to the design of equational laws for a subset of ML with references.

cs.LO↗

arXiv2023

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

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 yet been formalized in proof assistants based on dependent type theory: by extension of a measure over a semiring of sets. We achieve this formalization by leveraging on existing techniques from the Mathematical Components project. We explain how we extend Mathematical Components' iterated operators and mathematical structures for analysis to provide support for infinite sums and extended real numbers. We introduce new mathematical structures for measure theory and incidentally provide an illustrative, concrete application of Hierarchy-Builder, a generic tool for the formalization of hierarchies of mathematical structures. This formalization of measure theory provides the basis for a new formalization of the Lebesgue integration compatible with the Mathematical Components project.

cs.LO↗

arXiv2021

Extending Equational Monadic Reasoning with Monad Transformers

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 standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existing theory of modular monad transformers, which provides a uniform treatment of operations. Using this theory, we simplify the formalization of models in Monae and we propose an approach to support monadic equational reasoning in the presence of monad transformers. We also use Monae to revisit the lifting theorems of modular monad transformers by providing equational proofs and explaining how to patch a known bug using a non-standard use of Coq that combines impredicative polymorphism and parametricity.

cs.LO↗

arXiv2020

A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism

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 formalization in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a non-trivial interface which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories, and that we integrate in a framework for monadic equational reasoning.

cs.LO↗

arXiv2020

Formal Adventures in Convex and Conical Spaces

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 in vector spaces, we formalize in Coq an intrinsic axiomatization of convex sets, namely convex spaces, based on an operation taking barycenters of points. A convex space corresponds to a specific type that does not refer to a surrounding vector space. This simplifies the definitions of functions on it. We show applications including the convexity of information-theoretic functions defined over types of distributions. We also show how convex spaces are embedded in conical spaces, which are abstract real cones, and use the embedding as an effective device to ease calculations.

cs.LO↗

arXiv2019

Proving tree algorithms for succinct data structures

Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely one cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different tree-based succinct representations and their accompanying algorithms. One is the Level-Order Unary Degree Sequence, which encodes the structure of a tree in breadth-first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary balanced trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient insertion and deletion. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.

cs.PL↗