default search action
Reynald Affeldt
Person information
- affiliation: National Institute of Advanced Industrial Science and Technology, AIST, Japan
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c30]Reynald Affeldt
, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark:
Taming Differentiable Logics with Coq Formalisation. ITP 2024: 4:1-4:19 - [c29]Reynald Affeldt
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. ITP 2024: 5:1-5:19 - [c28]Reynald Affeldt
Robust Mean Estimation by All Means (Short Paper). ITP 2024: 39:1-39:8 - [d1]Natalia Slusarz
Formalisation of Differentiable Logics in Coq. DROPS Artifacts, 2024 - [i9]Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark:
Taming Differentiable Logics with Coq Formalisation. CoRR abs/2403.13700 (2024) - [i8]Reynald Affeldt, Zachary Stone:
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. CoRR abs/2403.18229 (2024) - 2023
- [j12]Reynald Affeldt
Measure Construction by Extension in Dependent Type Theory with Application to Integration. J. Autom. Reason. 67(3): 28 (2023) - [c27]Ayumu Saito
Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq. APLAS 2023: 182-202 - [c26]Reynald Affeldt
Semantics of Probabilistic Programs using s-Finite Kernels in Coq. CPP 2023: 3-16 - [i7]Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa:
A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory. CoRR abs/2312.06103 (2023) - 2022
- [c25]Ayumu Saito, Reynald Affeldt
Towards a Practical Library for Monadic Equational Reasoning in Coq. MPC 2022: 151-177 - [i6]Reynald Affeldt, Cyril Cohen:
Measure Construction by Extension in Dependent Type Theory with Application to Integration. CoRR abs/2209.02345 (2022) - 2021
- [j11]Reynald Affeldt
A trustful monad for axiomatic reasoning with probability and nondeterminism. J. Funct. Program. 31: e17 (2021) - 2020
- [j10]Reynald Affeldt
A Library for Formalization of Linear Error-Correcting Codes. J. Autom. Reason. 64(6): 1123-1164 (2020) - [c24]Reynald Affeldt, Cyril Cohen
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. IJCAR (2) 2020: 3-20 - [c23]Reynald Affeldt
Formal Adventures in Convex and Conical Spaces. CICM 2020: 23-38 - [c22]Reynald Affeldt
Extending Equational Monadic Reasoning with Monad Transformers. TYPES 2020: 2:1-2:21 - [i5]Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa:
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism. CoRR abs/2003.09993 (2020) - [i4]Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa:
Formal Adventures in Convex and Conical Spaces. CoRR abs/2004.12713 (2020) - [i3]Reynald Affeldt, David Nowak:
Extending Equational Monadic Reasoning with Monad Transformers. CoRR abs/2011.03463 (2020)
2010 – 2019
- 2019
- [c21]Reynald Affeldt
Proving Tree Algorithms for Succinct Data Structures. ITP 2019: 5:1-5:19 - [c20]Reynald Affeldt
A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. MPC 2019: 226-254 - [i2]Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka:
Proving tree algorithms for succinct data structures. CoRR abs/1904.02809 (2019) - 2018
- [j9]Reynald Affeldt
Formalization Techniques for Asymptotic Reasoning in Classical Analysis. J. Formaliz. Reason. 11(1): 43-76 (2018) - [j8]Akira Tanaka, Reynald Affeldt
Safe Low-level Code Generation in Coq Using Monomorphization and Monadification. J. Inf. Process. 26: 54-72 (2018) - [c19]Reynald Affeldt
Examples of Formal Proofs about Data Compression. ISITA 2018: 633-637 - 2017
- [c18]Reynald Affeldt
Formal foundations of 3D geometry to model robot manipulators. CPP 2017: 30-42 - 2016
- [c17]Akira Tanaka, Reynald Affeldt
Formal Verification of the rank Algorithm for Succinct Data Structures. ICFEM 2016: 243-260 - [c16]Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa:
Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. ISITA 2016: 532-536 - 2015
- [c15]Reynald Affeldt
Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory. ITP 2015: 17-33 - 2014
- [j7]Reynald Affeldt
Formalization of Shannon's Theorems. J. Autom. Reason. 53(1): 63-103 (2014) - [j6]Reynald Affeldt
An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing. J. Formaliz. Reason. 7(1): 63-104 (2014) - [c14]Ryosuke Obi, Manabu Hagiwara, Reynald Affeldt:
Formalization of the variable-length source coding theorem: Direct part. ISITA 2014: 201-205 - [c13]Yoichi Hirai, Reynald Affeldt:
What could Coq do for Database Software? - A Progress Report. JFLA 2014: 33-48 - 2013
- [j5]Reynald Affeldt
On construction of a library of formally verified low-level arithmetic functions. Innov. Syst. Softw. Eng. 9(2): 59-77 (2013) - [c12]Reynald Affeldt
Towards formal verification of TLS network packet processing written in C. PLPV 2013: 35-46 - 2012
- [j4]Reynald Affeldt
Certifying assembly with formal security proofs: The case of BBS. Sci. Comput. Program. 77(10-11): 1058-1074 (2012) - [c11]Reynald Affeldt
Formalization of Shannon's Theorems in SSReflect-Coq. ITP 2012: 233-249 - [c10]Reynald Affeldt
Formal network packet processing with minimal fuss: invertible syntax descriptions at work. PLPV 2012: 27-36 - [c9]Reynald Affeldt
On construction of a library of formally verified low-level arithmetic functions. SAC 2012: 1326-1331
2000 – 2009
- 2009
- [j3]Reynald Affeldt
Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 23 (2009) - [j2]Nicolas Marti, Reynald Affeldt:
A Certified Verifier for a Fragment of Separation Logic. Inf. Media Technol. 4(2): 304-316 (2009) - [c8]Reynald Affeldt
Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables. Formal to Practical Security 2009: 1-20 - [i1]Reynald Affeldt, David Nowak, Kiyoshi Yamada:
Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. IACR Cryptol. ePrint Arch. 2009: 322 (2009) - 2007
- [c7]Reynald Affeldt
Formal Proof of Provable Security by Game-Playing in a Proof Assistant. ProvSec 2007: 151-168 - 2006
- [c6]Reynald Affeldt
An Approach to Formal Verification of Arithmetic Functions in Assembly. ASIAN 2006: 346-360 - [c5]Nicolas Marti, Reynald Affeldt
Formal Verification of the Heap Manager of an Operating System Using Separation Logic. ICFEM 2006: 400-419 - 2004
- [j1]Frédéric Peschanski, Reynald Affeldt, Jean-Pierre Briot
Les espaces d'interaction Vers une géométrie des systèmes d'agents mobiles. Obj. Logiciel Base données Réseaux 10(2-3): 31-45 (2004) - [c4]Reynald Affeldt
A Coq Library for Verification of Concurrent Programs. LFM@IJCAR 2004: 17-32 - [c3]Reynald Affeldt
Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes. EXPRESS 2004: 151-168 - 2002
- [c2]Reynald Affeldt
Formalization and Verification of a Mail Server in Coq. ISSS 2002: 217-233 - [c1]Reynald Affeldt
Supporting objects in run-time bytecode specialization. ASIA-PEPM 2002: 50-60
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-15 20:50 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: