@article{affeldt2025topml,
author = {Reynald Affeldt and Cyril Cohen and Ayumu Saito},
title = {Semantics of Probabilistic Programs using s-Finite Kernels in Dependent Type Theory},
journal = {\href{https://dl.acm.org/journal/topml}{ACM Transactions on Probabilistic Machine Learning}},
year = {2025},
volume = {1},
number = {3},
pages = {16:1--16:34},
abstract = {\href{https://dl.acm.org/doi/10.1145/3732291}{open access} \href{http://dx.doi.org/10.1145/3732291}{doi}}
}
@article{affeldt2025jfp,
author = {Reynald Affeldt and Jacques Garrigue and Takafumi Saikawa},
title = {A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory},
journal = {\href{https://www.cambridge.org/core/journals/journal-of-functional-programming}{Journal of Functional Programming}},
year = {2025},
volume = {35},
number = {e1},
pages = {1--40},
abstract = {\href{https://www.cambridge.org/core/journals/journal-of-functional-programming/article/practical-formalization-of-monadic-equational-reasoning-in-dependenttype-theory/B59B87DE000F48B9807F24AEDB11452E}{open access} \href{http://dx.doi.org/10.1017/S0956796824000157}{doi}}
}
@article{ishiguro2024cs,
author = {Yoshihiro Ishiguro and Reynald Affeldt},
title = {The {Radon}-{Nikod}{\'y}m Theorem and the {Lebesgue}-{Stieltjes} Measure in {Coq}},
journal = {\href{https://www.jstage.jst.go.jp/browse/jssst}{Computer Software}},
year = {2024},
volume = {41},
number = {2},
pages = {41--59},
abstract = {\href{https://www.jstage.jst.go.jp/article/jssst/41/2/41_2_41/_article/-char/en}{open access} \href{http://dx.doi.org/10.11309/jssst.41.2_41}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/cs2024_preprint.pdf}{pdf preprint}}
}
@article{affeldt2023jar,
author = {Reynald Affeldt and Cyril Cohen},
title = {Measure Construction by Extension in Dependent Type Theory with Application to Integration},
journal = {\href{https://www.springer.com/journal/10817/}{Journal of Automated Reasoning}},
year = {2023},
volume = {67},
number = {3},
pages = {28:1--28:27},
abstract = {\href{http://dx.doi.org/10.1007/s10817-023-09671-5}{doi} arXiv: \href{https://arxiv.org/abs/2209.02345}{cs.LO 2209.02345}},
doi = {10.1007/s10817-023-09671-5}
}
@article{affeldt2021jfp,
author = {Reynald Affeldt and Jacques Garrigue and David Nowak and Takafumi Saikawa},
title = {A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism},
journal = {\href{https://www.cambridge.org/core/journals/journal-of-functional-programming}{Journal of Functional Programming}},
year = {2021},
volume = {31},
number = {E17},
pages = {},
abstract = {\href{http://dx.doi.org/10.1017/S0956796821000137}{doi} arXiv: \href{https://arxiv.org/abs/2003.09993}{cs.LO 2003.09993}},
doi = {10.1017/S0956796821000137}
}
@article{affeldt2020cs,
author = {Reynald Affeldt and Jacques Garrigue and Takafumi Saikawa},
title = {Reasoning with Conditional Probabilities and Joint Distributions in {Coq}},
journal = {\href{https://www.jstage.jst.go.jp/browse/jssst}{Computer Software}},
year = {2020},
volume = {37},
number = {3},
pages = {79--95},
abstract = {\href{https://www.jstage.jst.go.jp/article/jssst/37/3/37_3_79/_article/-char/en}{open access} \href{http://dx.doi.org/10.11309/jssst.37.3_79}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/cproba_preprint.pdf}{pdf preprint} \href{https://github.com/affeldt-aist/infotheo}{project page}}
}
@article{affeldt2020jar,
author = {Reynald Affeldt and Jacques Garrigue and Takafumi Saikawa},
title = {A Library for Formalization of Linear Error-correcting Codes},
journal = {\href{https://link.springer.com/journal/10817}{Journal of Automated Reasoning}},
year = {2020},
volume = {64},
number = {},
pages = {1123--1164},
abstract = {\href{http://dx.doi.org/10.1007/s10817-019-09538-8}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/ecc.pdf}{pdf preprint} \href{https://github.com/affeldt-aist/infotheo}{project page}}
}
@article{cohen2018jfr,
author = {Reynald Affeldt and Cyril Cohen and Damien Rouhling},
title = {Formalization Techniques for Asymptotic Reasoning in Classical Analysis},
journal = {\href{https://jfr.unibo.it/}{Journal of Formalized Reasoning}},
year = {2018},
volume = {11},
number = {1},
pages = {43--76},
abstract = {\href{https://jfr.unibo.it/article/view/8124}{open access} \href{http://dx.doi.org/10.6092/issn.1972-5787/8124}{doi} \href{https://github.com/math-comp/analysis}{project page}},
doi = {}
}
@article{tanaka2017jip,
author = {Akira Tanaka and Reynald Affeldt and Jacques Garrigue},
title = {Safe Low-level Code Generation in {Coq} using Monomorphization and Monadification},
journal = {\href{http://www.ipsj.or.jp/english/jip/}{Journal of Information Processing}},
year = {2018},
volume = {26},
number = {},
pages = {54--72},
abstract = {Reprinted from IPSJ Transactions on Programming 10(6), 2017 \href{https://www.jstage.jst.go.jp/article/ipsjjip/26/0/26_54/_pdf/-char/en}{open access} \href{http://dx.doi.org/10.2197/ipsjjip.26.54}{doi} \href{https://staff.aist.go.jp/tanaka-akira/succinct/}{project page}}
}
@article{affeldt2014jfr,
author = {Reynald Affeldt and Kazuhiko Sakaguchi},
title = {An Intrinsic Encoding of a Subset of {C} and its Application to {TLS} Network Packet Processing},
journal = {\href{https://jfr.unibo.it/index}{Journal of Formalized Reasoning}},
year = {2014},
volume = {7},
number = {1},
pages = {63--104},
abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/vtls-long.pdf}{pdf preprint} \href{https://jfr.unibo.it/article/download/4317/3950}{open access} \href{http://dx.doi.org/10.6092/issn.1972-5787/4317}{doi} \href{https://staff.aist.go.jp/reynald.affeldt/seplog/}{project page}}
}
@article{affeldt2014jar,
author = {Reynald Affeldt and Manabu Hagiwara and Jonas S\'enizergues},
title = {Formalization of {Shannon}'s Theorems},
journal = {\href{https://link.springer.com/journal/10817}{Journal of Automated Reasoning}},
year = {2014},
volume = {53},
number = {1},
pages = {63--103},
abstract = {\href{http://dx.doi.org/10.1007/s10817-013-9298-1}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/shannon_theorems.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/shannon/}{project page}}
}
@article{affeldt2013isse,
author = {Reynald Affeldt},
title = {On Construction of a Library of Formally Verified Low-level Arithmetic Functions},
journal = {\href{http://www.springer.com/computer/swe/journal/11334}{Innovations in Systems and Software Engineering}},
year = {2013},
volume = {9},
number = {2},
pages = {59--77},
abstract = {NASA/Springer \href{http://dx.doi.org/10.1007/s11334-013-0195-x}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/arilib-affeldt-long.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/seplog/}{project page}}
}
@article{affeldt2012scp,
author = {Reynald Affeldt and David Nowak and Kiyoshi Yamada},
title = {Certifying Assembly with Formal Security Proofs: the Case of {BBS}},
journal = {\href{https://www.sciencedirect.com/journal/science-of-computer-programming}{Science of Computer Programming}},
year = {2012},
volume = {77},
number = {10--11},
pages = {1058--1074},
abstract = {\href{http://dx.doi.org/10.1016/j.scico.2011.07.003}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-bbs.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/bbs/}{project page}}
}
@inproceedings{affeldt2009rigid,
author = {Reynald Affeldt and Hubert Comon-Lundh},
title = {Verification of Security Protocols with a Bounded Number of Sessions based on Resolution for Rigid Variables},
booktitle = {Formal to Practical Security},
year = {2009},
editor = {},
volume = {5458},
series = {Lecture Notes in Computer Science, State-of-the-Art Survey},
pages = {1--20},
month = {May},
publisher = {Springer},
abstract = {\href{http://dx.doi.org/10.1007/978-3-642-02002-5_1}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/rigid.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/rigid/}{project page}}
}
@article{marti2008compsoft,
author = {Nicolas Marti and Reynald Affeldt},
title = {A Certified Verifier for a Fragment of Separation Logic},
journal = {\href{https://www.jstage.jst.go.jp/browse/jssst}{Computer Software}},
year = {2008},
volume = {25},
number = {3},
pages = {135--147},
abstract = {Japan Society for Software Science and Technology. Iwanami Shoten \href{https://www.jstage.jst.go.jp/article/jssst/25/3/25_3_3_135/_pdf}{open access} \href{http://dx.doi.org/10.11309/jssst.25.3_135}{doi} \href{https://staff.aist.go.jp/reynald.affeldt/seplog/}{project page} Reprinted to \href{https://www.jstage.jst.go.jp/browse/imt}{Information and Media Technologies} 4(2):304--316, 2009 \href{http://dx.doi.org/10.11185/imt.4.304}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/cs2007.pdf}{pdf preprint}}
}
@article{affeldt2005ipsj,
author = {Reynald Affeldt and Naoki Kobayashi and Akinori Yonezawa},
title = {Verification of concurrent programs using the {Coq} proof assistant: a case study},
journal = {IPSJ Transactions on Programming},
year = {2005},
volume = {46},
number = {SIG1(PRO24)},
pages = {110--120},
abstract = {Information Processing Society of Japan. Reprinted to \href{https://www.ipsj.or.jp/08editt/dc/index.html}{IPSJ Digital Courier} 1:117--127, 2005 \href{https://www.jstage.jst.go.jp/article/ipsjdc/1/0/1_0_117/_pdf}{open access} \href{http://dx.doi.org/10.2197/ipsjdc.1.117}{doi} \href{http://staff.aist.go.jp/reynald.affeldt/documents/swopp04.pdf}{pdf preprint} \href{https://staff.aist.go.jp/reynald.affeldt/applpi/}{project page}}
}
This file was generated by bibtex2html 1.99.