Zobrazeno 1 - 10
of 50
pro vyhledávání: '"Affeldt , Reynald"'
Autor:
Affeldt, Reynald, Stone, Zachary
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 formal
Externí odkaz:
http://arxiv.org/abs/2403.18229
Autor:
Affeldt, Reynald, Bruni, Alessandro, Komendantskaya, Ekaterina, Ślusarz, Natalia, Stark, Kathrin
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 prop
Externí odkaz:
http://arxiv.org/abs/2403.13700
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
Externí odkaz:
http://arxiv.org/abs/2312.06103
Autor:
Affeldt, Reynald, Cohen, Cyril
Publikováno v:
Journal of Automated Reasoning, 67(3):28:1--28:27 2023
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:
Externí odkaz:
http://arxiv.org/abs/2209.02345
Autor:
Affeldt, Reynald, Nowak, David
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
Externí odkaz:
http://arxiv.org/abs/2011.03463
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 co
Externí odkaz:
http://arxiv.org/abs/2004.12713
Publikováno v:
Journal of Functional Programming, 31(E17), 2021
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
Externí odkaz:
http://arxiv.org/abs/2003.09993
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 dif
Externí odkaz:
http://arxiv.org/abs/1904.02809
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
Affeldt, Reynald, Cohen, Cyril, Kerjean, Marie, Mahboubi, Assia, Rouhling, Damien, Sakaguchi, Kazuhiko
Publikováno v:
Automated Reasoning
This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topology and norms, in dependent type theory. This hierarchy is the backbone of a new library of formalized classical anal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=pmc_________::664bfd2ba25b8139bfc0a322a7c947df
http://europepmc.org/articles/PMC7324078
http://europepmc.org/articles/PMC7324078
