[1] 
Yoshihiro Ishiguro and Reynald Affeldt.
The RadonNikodým theorem and the LebesgueStieltjes
measure in Coq.
Computer
Software, 2024.
[ bib ]
To appear. pdf preprint 
[2] 
Reynald Affeldt and Cyril Cohen.
Measure construction by extension in dependent type theory with
application to integration.
Journal of
Automated Reasoning, 67(3):28:128:27, 2023.
[ bib ]
doi arXiv: cs.LO 2209.02345 
[3] 
Reynald Affeldt, Jacques Garrigue, David Nowak, and Takafumi Saikawa.
A trustful monad for axiomatic reasoning with probability and
nondeterminism.
Journal
of Functional Programming, 31(E17), 2021.
[ bib ]
doi arXiv: cs.LO 2003.09993 
[4] 
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa.
Reasoning with conditional probabilities and joint distributions in
Coq.
Computer
Software, 37(3):7995, 2020.
[ bib ]
open access doi pdf preprint project page 
[5] 
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa.
A library for formalization of linear errorcorrecting codes.
Journal of
Automated Reasoning, 64:11231164, 2020.
[ bib ]
doi pdf preprint project page 
[6] 
Reynald Affeldt, Cyril Cohen, and Damien Rouhling.
Formalization techniques for asymptotic reasoning in classical
analysis.
Journal of Formalized Reasoning,
11(1):4376, 2018.
[ bib ]
open access doi project page 
[7] 
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue.
Safe lowlevel code generation in Coq using monomorphization and
monadification.
Journal of Information
Processing, 26:5472, 2018.
[ bib ]
Reprinted from IPSJ Transactions on Programming 10(6), 2017 open access doi project page 
[8] 
Reynald Affeldt and Kazuhiko Sakaguchi.
An intrinsic encoding of a subset of C and its application to TLS
network packet processing.
Journal of Formalized
Reasoning, 7(1):63104, 2014.
[ bib ]
pdf preprint open access doi project page 
[9] 
Reynald Affeldt, Manabu Hagiwara, and Jonas Sénizergues.
Formalization of Shannon's theorems.
Journal of
Automated Reasoning, 53(1):63103, 2014.
[ bib ]
doi pdf preprint project page 
[10] 
Reynald Affeldt.
On construction of a library of formally verified lowlevel
arithmetic functions.
Innovations in
Systems and Software Engineering, 9(2):5977, 2013.
[ bib ]
NASA/Springer doi pdf preprint project page 
[11] 
Reynald Affeldt, David Nowak, and Kiyoshi Yamada.
Certifying assembly with formal security proofs: the case of BBS.
Science
of Computer Programming, 77(1011):10581074, 2012.
[ bib ]
doi pdf preprint project page 
[12] 
Reynald Affeldt and Hubert ComonLundh.
Verification of security protocols with a bounded number of sessions
based on resolution for rigid variables.
In Formal to Practical Security, volume 5458 of Lecture
Notes in Computer Science, StateoftheArt Survey, pages 120. Springer,
May 2009.
[ bib ]
doi pdf preprint project page 
[13] 
Nicolas Marti and Reynald Affeldt.
A certified verifier for a fragment of separation logic.
Computer
Software, 25(3):135147, 2008.
[ bib ]
Japan Society for Software Science and Technology. Iwanami Shoten open access doi project page Reprinted to Information and Media Technologies 4(2):304316, 2009 doi pdf preprint 
[14] 
Reynald Affeldt, Naoki Kobayashi, and Akinori Yonezawa.
Verification of concurrent programs using the Coq proof assistant:
a case study.
IPSJ Transactions on Programming, 46(SIG1(PRO24)):110120,
2005.
[ bib ]
Information Processing Society of Japan. Reprinted to IPSJ Digital Courier 1:117127, 2005 open access doi pdf preprint project page 
[1] 
Reynald Affeldt and Ayumu Saito.
Experimenting with an intrinsicallytyped probabilistic programming
language in Coq.
In 21st Asian Symposium on Programming Languages and Systems
(APLAS 2023), Taipei,
Taiwan, November 2629, 2023, volume 14405, pages 182202. Springer, Nov
2023.
[ bib ]
doi pdf preprint 
[2] 
Reynald Affeldt, Cyril Cohen, and Ayumu Saito.
Semantics of probabilistic programs using sfinite kernels in Coq.
In 12th ACM SIGPLAN Conference on Certified Programs and Proofs
(CPP 2023), Boston, MA, USA,
January 1617, 2023, pages 316. ACM Press, Jan 2023.
[ bib ]
doi open access 
[3] 
Ayumu Saito and Reynald Affeldt.
Towards a practical library for monadic equational reasoning in
Coq.
In 14th International Conference on Mathematics of Program
Construction (MPC 2022), Tbilisi,
Georgia, September 2628, 2022, volume 13544 of Lecture Notes in
Computer Science, pages 151177. Springer, Sep 2022.
[ bib ]
pdf preprint doi project page 
[4] 
Reynald Affeldt and David Nowak.
Extending equational monadic reasoning with monad transformers.
In 26th International Conference on Types for Proofs and
Programs (TYPES 2020), volume 188 of
Leibniz International Proceedings in Informatics, pages 2:12:21.
Schloss Dagstuhl, Jun 2021.
[ bib ]
doi PostProceedings. arXiv preprint cs.LO 2011.03463 
[5] 
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa.
Formal adventures in convex and conical spaces.
In 13th Conference on Intelligent Computer Mathematics
(CICM 2020), Bertinoro, Forli,
Italy, July 2631, 2020, volume 12236 of Lecture Notes in Artificial
Intelligence, pages 2338. Springer, Jul 2020.
[ bib ]
doi open access 
[6] 
Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling,
and Kazuhiko Sakaguchi.
Competing inheritance paths in dependent type theory: a case study in
functional analysis.
In 10th International Joint Conference on Automated Reasoning
(IJCAR 2020), Paris, France, June 29July 6,
2020, volume 12167 of Lecture Notes in Artificial Intelligence, pages
320. Springer, Jul 2020.
[ bib ]
doi open access 
[7] 
Reynald Affeldt, David Nowak, and Takafumi Saikawa.
A hierarchy of monadic effects for program verification using
equational reasoning.
In 13th International Conference on Mathematics of Program
Construction (MPC 2019),
Porto, Portugal, October 79, 2019, volume 11825 of Lecture Notes in
Computer Science, pages 226254. Springer, Oct 2019.
[ bib ]
doi pdf preprint project page 
[8] 
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka.
Proving tree algorithms for succinct data structures.
In 10th International Conference on Interactive Theorem Proving
(ITP 2019), Portland, OR, USA, September
813, 2019, volume 141 of Leibniz International Proceedings in
Informatics, pages 28:128:19. Schloss Dagstuhl, Sep 2019.
[ bib ]
open access doi pdf preprint project page 
[9] 
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa.
Examples of formal proofs about data compression.
In International Symposium on Information Theory and Its
Applications (ISITA 2018),
Singapore, October 2831, 2018, pages 633637. IEEE, Oct 2018.
[ bib ]
doi pdf preprint project page 
[10] 
Reynald Affeldt and Cyril Cohen.
Formal foundations of 3D geometry to model robot manipulators.
In 6th ACM SIGPLAN Conference on Certified Programs and Proofs
(CPP 2017), Paris, France, January
1617, 2017, pages 3042. ACM Press, Jan 2017.
[ bib ]
doi pdf preprint project page slides 
[11] 
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue.
Formal verification of the rank algorithm for succinct data
structures.
In 18th International Conference on Formal Engineering Methods
(ICFEM 2016), Tokyo, Japan, November 1418, 2016, volume 10009 of
Lecture Notes in Computer Science, pages 243260. Springer, Nov 2016.
[ bib ]
doi pdf preprint project page 
[12] 
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa.
Formalization of ReedSolomon codes and progress report on
formalization of LDPC codes.
In International Symposium on Information Theory and Its
Applications (ISITA 2016),
Monterey, California, USA, October 30November 2, 2016, pages 537541.
IEICE. IEEE Xplore, Oct 2016.
[ bib ]
doi pdf preprint project page 
[13] 
Reynald Affeldt and Jacques Garrigue.
Formalization of errorcorrecting codes: from Hamming to modern
coding theory.
In 6th Conference on Interactive Theorem Proving
(ITP 2015), Nanjing,
China, August 2427, 2015, volume 9236 of Lecture Notes in Computer
Science, pages 1733. Springer, Aug 2015.
[ bib ]
doi pdf preprint project page 
[14] 
Ryosuke Obi, Manabu Hagiwara, and Reynald Affeldt.
Formalization of variablelength source coding theorem: Direct part.
In International Symposium on Information Theory and Its
Applications (ISITA 2014), Melbourne, Australia, October 2629, 2014, pages
201205. IEICE. IEEE Xplore, Oct 2014.
[ bib ]

[15] 
Reynald Affeldt and Nicolas Marti.
Towards formal verification of TLS network packet processing
written in C.
In 7th ACM SIGPLAN Workshop on Programming Languages meets
Program Verification (PLPV 2013), Rome,
Italy, January 22, 2013, pages 3546. ACM Press, Jan 2013.
[ bib ]
doi pdf preprint 
[16] 
Reynald Affeldt and Manabu Hagiwara.
Formalization of Shannon's theorems in SSReflectCoq.
In 3rd Conference on Interactive Theorem Proving
(ITP 2012), Princeton, New Jersey,
USA, August 1315, 2012, volume 7406 of Lecture Notes in Computer
Science, pages 233249. Springer, Aug 2012.
[ bib ]
doi pdf preprint project page slides 
[17] 
Reynald Affeldt.
On construction of a library of formally verified lowlevel
arithmetic functions.
In 27th ACM SIGAPP Symposium On Applied Computing
(SAC 2012), Riva del Garda
(Trento), Italy, March 2630, 2012, volume 2, pages 13261331. ACM Press,
Mar 2012.
[ bib ]
pdf preprint doi Software Verification and Testing Track project page 
[18] 
Reynald Affeldt, David Nowak, and Yutaka Oiwa.
Formal network packet processing with minimal fuss: Invertible syntax
descriptions at work.
In 6th ACM SIGPLAN Workshop on Programming Languages meets
Program Verification (PLPV 2012), Philadelphia, USA, January 24, 2012, pages
2736. ACM Press, Jan 2012.
[ bib ]
pdf preprint doi 
[19] 
Reynald Affeldt, David Nowak, and Kiyoshi Yamada.
Certifying assembly with formal cryptographic proofs: the case of
BBS.
In
Electronic
Communications of the EASST, volume 23. European Association of Software
Science and Technology, Jan 2010.
[ bib ]
doi pdf preprint project page Proceedings of the 9th International Workshop on Automated Verification of Critical Systems (AVoCS 2009), Swansea University Computer Science, September 2325, 2009. Preliminary version: Technical Report of Computer Science, Swansea University CSR22009 
[20] 
Reynald Affeldt and Hubert ComonLundh.
A note on firstorder logic and security protocols.
In Joint Workshop on Foundations of Computer Security, Automated
Reasoning for Security Protocol Analysis and Issues in the Theory of Security
(FCSARSPAWITS
2008), Pittsburgh, PA, USA, June 2122, 2008, pages 1120, Jun 2008.
[ bib ]
pdf preprint project page 
[21] 
Reynald Affeldt, Miki Tanaka, and Nicolas Marti.
Formal proof of provable security by gameplaying in a proof
assistant.
In 1st International Conference on Provable Security (Provsec
2007), Wollongong, NSW, Australia, November 12, 2007, volume 4784 of
Lecture Notes in Computer Science, pages 151168. Springer, Nov 2007.
[ bib ]
doi pdf preprint 
[22] 
Reynald Affeldt and Nicolas Marti.
An approach to formal verification of arithmetic functions in
assembly.
In 11th Annual Asian Computing Science Conference (ASIAN 2006),
Focusing on Secure Software and Related Issues, Tokyo, Japan, December 68,
2006, volume 4435 of Lecture Notes in Computer Science, pages
346360. Springer, Jan 2008.
[ bib ]
doi pdf preprint project page 
[23] 
Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa.
Formal verification of the heap manager of an operating system using
separation logic.
In 8th International Conference on Formal Engineering Methods
(ICFEM 2006), Macao SAR, China, October 29November 3, 2006, volume 4260 of
Lecture Notes in Computer Science, pages 400419. Springer, Oct 2006.
[ bib ]
doi pdf preprint 
[24] 
Reynald Affeldt and Naoki Kobayashi.
Partial order reduction for verification of spatial properties of
picalculus processes.
Electronic Notes in Theoretical Computer Science,
128(2):151168, Apr 2005.
[ bib ]
doi Elsevier. Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS 2004), London, UK, August 30, 2004 pdf preprint pdf preprint 
[25] 
Reynald Affeldt and Naoki Kobayashi.
A Coq library for verification of concurrent programs.
Electronic Notes in Theoretical Computer Science, 199:1732,
Feb 2008.
[ bib ]
doi pdf preprint project page Elsevier. Proceedings of the 4th International Workshop on Logical Frameworks and MetaLanguages (LFM 2004), Cork, Ireland, July 5, 2004 
[26] 
Reynald Affeldt and Naoki Kobayashi.
Formalization and verification of a mail server in Coq.
In International Symposium on Software Security, Tokyo, Japan,
November 810, 2002, volume 2609 of Lecture Notes in Computer Science,
Hot Topics, pages 217233. Springer, Feb 2003.
[ bib ]
doi pdf preprint slides 
[27] 
Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, and Akinori Yonezawa.
Supporting objects in runtime bytecode specialization.
In ACM SIGPLAN Asian Symposium on Partial Evaluation and
Semanticsbased Program Manipulation (ASIAPEPM 2002), Aizu, Japan, September
1214, 2002, pages 5060. ACM Press, Sep 2002.
[ bib ]
doi pdf preprint slides 
[1] 
Ayumu Saito and Reynald Affeldt.
An intrinsicallytyped probabilistic programming language in Coq
(extended abstract).
The Workshop on TypeDriven Development (TyDe 2023), Seattle,
Washington, United States, September 4, 2023, Sep 2023.
[ bib ]
pdf preprint open access 
[2] 
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa.
Environmentfriendly monadic equational reasoning for OCaml.
The Coq Workshop 2023, Białystok, Poland, July 31, 2023, Jul 2023.
[ bib ]
pdf preprint project page open access 
[3] 
Reynald Affeldt and Cyril Cohen.
Formalization of the Lebesgue measure in MathCompAnalysis.
The Coq Workshop 2021, online, July 2, 2021, Jul 2021.
[ bib ]
pdf preprint project page open access 
[4] 
Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen,
Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry, and Anton
Trunov.
Porting the Mathematical Components library to Hierarchy Builder.
The Coq Workshop 2021, online, July 2, 2021, Jul 2021.
[ bib ]
open access 
[5] 
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka.
Experience report: Typedriven development of certified tree
algorithms in Coq.
The Coq Workshop 2019, Portland, OR, USA, September 8, 2019, Sep
2019.
[ bib ]
open access 
[6] 
Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, and PierreYves
Strub.
Classical analysis with Coq.
The Coq Workshop 2018, Oxford, UK, July 8, 2018, Jul 2018.
[ bib ]
project page pdf preprint 
[7] 
Reynald Affeldt and Jacques Garrigue.
Formalization of errorcorrecting codes using SSReflect.
The 6th Coq Workshop, Vienna, Austria, July 7, 2014, Jul 2014.
[ bib ]
project page 
[8] 
Reynald Affeldt and Kazuhiko Sakaguchi.
First building blocks for implementations of security protocols
verified in Coq.
The 5th Coq Workshop, Rennes, France, July 22, 2013, Jul 2013.
[ bib ]
project page 
[9] 
Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa.
Verification of the heap manager of an operating system using
separation logic.
The 3rd Workshop on Semantics, Program Analysis, and Computing
Environments for Memory Management (SPACE 2006), Charleston SC, USA, January
14, 2006, Jan 2006.
[ bib ]
pdf preprint Informal proceedings. Pages 6172 slides project page 
[1] 
Reynald Affeldt and Zachary Stone.
Towards the fundamental theorem of calculus for the Lebesgue
integral in Coq.
In 35st Journées Francophones des Langages Applicatifs (JFLA
2024), SaintJacutdelaMer, France, January 30February 2, pages
300304. Inria and others, Jan 2024.
[ bib ]
open access 
[2] 
Yoshihiro Ishiguro and Reynald Affeldt.
A progress report on formalization of measure theory with
MathCompAnalysis.
In 25th Workshop on Programming and Programming Languages
(PPL2023), Nagoya University, March 68, 2023, Mar 2023.
[ bib ]
15 pages. pdf preprint conference website 
[3] 
Ayumu Saito and Reynald Affeldt.
Practical aspects of monadic equational reasoning in Coq.
In 24th Workshop on Programming and Programming Languages
(PPL2022), March 68, 2022, Mar 2022.
[ bib ]
17 pages. pdf preprint conference website 
[4] 
Célestine Sauvage, Reynald Affeldt, and David Nowak.
Vers la formalisation en Coq des transformateurs de monades
modulaires.
In 31st Journées Francophones des Langages Applicatifs (JFLA
2020), Gruissan, France, January 29February 1, pages 2330. CEA List and
others, Jan 2020.
[ bib ]
pdf preprint open access 
[5] 
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa.
Reasoning with conditional probabilities and joint distributions in
Coq.
In 21st Workshop on Programming and Programming Languages
(PPL2019), Iwateken, Hanamakishi, March 68, 2019, Mar 2019.
[ bib ]
16 pages. pdf preprint conference website 
[6] 
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue.
Formal verification of the rank function for succinct data
structures.
In 18th Workshop on Programming and Programming Languages
(PPL2016), Okayamaken, Tamanoshi, March 79, 2016, Mar 2016.
[ bib ]
15 pages. Best paper award conference website project page 
[7] 
Yoichi Hirai and Reynald Affeldt.
What could Coq do for database software?a progress report.
In 25th Journées Francophones des Langages Applicatifs (JFLA
2014), Fréjus, France, January 811, pages 3348, Jan 2014.
[ bib ]

[8] 
Reynald Affeldt.
Toward formal construction of assembly arithmetic functions from
pseudocode.
In 12th Workshop on Programming and Programming Languages
(PPL2010), Kagawaken, Kotohira Onsen, March 35, 2010, pages 114, Mar
2010.
[ bib ]
pdf preprint conference website project page 
[9] 
Nicolas Marti and Reynald Affeldt.
A certified verifier for a fragment of separation logic.
In 9th Workshop on Programming and Programming Languages
(PPL2007), Ishikawaken, Kagashi, March 810, 2007, pages 187199, Mar
2007.
[ bib ]
Best paper award project page 
[1] 
Reynald Affeldt and David Nowak.
Experimenting with monadic equational reasoning in Coq.
In the proceedings of the 35th Meeting of the Japan Society for
Software Science and Technology
(JSSST 2018), Osakafu, Suitashi,
August 2931, 2018, Aug 2018.
[ bib ]
14 pages project page pdf preprint 
[2] 
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka.
Proving tree algorithms for succinct data structures.
In the proceedings of the 35th Meeting of the Japan Society for
Software Science and Technology
(JSSST 2018), Osakafu, Suitashi,
August 2931, 2018, Aug 2018.
[ bib ]
13 pages project page pdf preprint 
[3] 
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue.
Extension of a C code generator for Coq with a linearity checker.
In the proceedings of the 35th Meeting of the Japan Society for
Software Science and Technology
(JSSST 2018), Osakafu, Suitashi,
August 2931, 2018, Aug 2018.
[ bib ]
11 pages (in Japanese) pdf preprint 
[4] 
Reynald Affeldt and Cyril Cohen.
Formal foundations for rigid body transformation.
In the proceedings of the 33rd Meeting of the Japan Society for
Software Science and Technology
(JSSST 2016), Miyagiken,
Sendaishi, September 69, 2016, Sep 2016.
[ bib ]
11 pages project page pdf preprint 
[5] 
Reynald Affeldt.
An intrinsic encoding of a subset of C and its application to TLS
network packet processing.
In Annual Workshop of the Japan Society for Industrial and
Applied Mathematics 2015, Kanazawa University, Kakuma campus, September 911,
2015, pages 306307, Sep 2015.
[ bib ]
project page pdf preprint 
[6] 
Reynald Affeldt and Jacques Garrigue.
Formalization of errorcorrecting codes using SSReflect.
In MI Lecture Note Workshop on Theorem proving and provers for
reliable theory and implementations (TPP2014), Kyushu University, December
35, 2014, volume 61, pages 7678, Dec 2014.
[ bib ]
project page 
[7] 
Reynald Affeldt.
Formalization of Shannon's theorems using the Coq
proofassistant.
In proceedings of the 2013 IEICE General Conference, The
Institute of Electronics, Information and Communication Engineers, Fukuoka
Institute of Technology, September 1720, 2013, pages 3944, Sep 2013.
[ bib ]
pdf preprint project page conference website IEICE, Technical Committee on Information Theory 
[8] 
Reynald Affeldt.
About the formal verification of Shannon's theorems.
In COE Lecture Note Kyushu University Institute of Mathematics
for Industry, Workshop of the Joint Research Projects: From Modern Coding
Theory To Postmodern Coding Theory, Kyushu University, March 47, 2013,
volume 44, pages 8694, Mar 2013.
[ bib ]
pdf preprint project page 
[9] 
Reynald Affeldt.
Toward a library of verified arithmetic functions.
In Annual Workshop of the Japan Society for Industrial and
Applied Mathematics 2011, Doshisha University, September 1416, 2011, pages
377378, Sep 2011.
[ bib ]
project page 
[10] 
Reynald Affeldt and Kiyoshi Yamada.
Formal verification of C programs for implementations of
communication protocols.
In the proceedings of the 28th Meeting of the Japan Society for
Software Science and Technology
(JSSST 2011), Okinawaken,
Nahashi, September 2629, 2011, Sep 2011.
[ bib ]
pdf preprint project page 
[11] 
Reynald Affeldt, David Nowak, and Kiyoshi Yamada.
Certifying assembly with formal cryptographic proofs: the case of
BBS.
In Annual Workshop of the Japan Society for Industrial and
Applied Mathematics 2009
(JSIAM 2009),
Osaka University, September 2830, 2009, pages 5354, Sep 2009.
[ bib ]
pdf preprint slides (in Japanese) project page 
[12] 
Reynald Affeldt and Hubert ComonLundh.
Towards verification with no false attack of security protocols in
firstorder logic.
In Annual Workshop of the Japan Society for Industrial and
Applied Mathematics 2008
(JSIAM 2008),
The University of Tokyo, Kashiwa campus, September 1719, 2008, pages
177178, Sep 2008.
[ bib ]
pdf preprint slides project page 
[13] 
Reynald Affeldt and Yusuke Kawamoto.
Report on FCSARSPAWITS, CSF, FCC'08about automated
verification and certification.
In Annual Workshop of the Japan Society for Industrial and
Applied Mathematics 2008, The University of Tokyo, Kashiwa campus, September
1719, 2008, pages 187188, Sep 2008.
[ bib ]

[14] 
Yusuke Kawamoto and Reynald Affeldt.
Report on FCSARSPAWITS, CSF, FCC'08about formalization of
security properties.
In Annual Workshop of the Japan Society for Industrial and
Applied Mathematics 2008, The University of Tokyo, Kashiwa campus, September
1719, 2008, pages 185186, Sep 2008.
[ bib ]
(in Japanese) 
[15] 
Reynald Affeldt, Miki Tanaka, and Nicolas Marti.
Formal proof of provable security by gameplaying in a proof
assistant.
In Annual Workshop of the Japan Society for Industrial and
Applied Mathematics 2017
(JSIAM 2007), Hokkaido
University, September 1517, 2007, pages 4445, Sep 2007.
[ bib ]
pdf preprint (in Japanese) 
[16] 
Reynald Affeldt and Nicolas Marti.
Formal verification of arithmetic functions in SmartMIPS assembly.
In the proceedings of the 23rd Meeting of the Japan Society for
Software Science and Technology, The University of Tokyo, Hongo campus,
September 1315, 2006, Sep 2006.
[ bib ]
pdf preprint project page 
[17] 
Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa.
Modelchecking of a multithreaded operating system.
In the proceedings of the 23rd Meeting of the Japan Society for
Software Science and Technology, The University of Tokyo, Hongo campus,
September 1315, 2006, Sep 2006.
[ bib ]
pdf preprint project page 
[18] 
Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa.
Towards formal verification of memory properties using separation
logic.
In the proceedings of the 22nd Meeting of the Japan Society for
Software Science and Technology, Tohoko University, Aobayama campus,
September 1315, 2005, Sep 2005.
[ bib ]
pdf preprint slides project page 
[19] 
Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, and Akinori Yonezawa.
Supporting objects in runtime bytecode specialization.
In the proceedings of the 18th Meeting of the Japan Society for
Software Science and Technology
(JSSST 2011), Future
University Hakodate, September 1820, 2001, Sep 2001.
[ bib ]
pdf preprint 
[1] 
Reynald Affeldt and Zachary Stone.
The fundamental theorem of calculus for the Lebesgue integral in
MathCompAnalysis.
Oct 2023.
[ bib ]
19th Theorem Proving and Provers Meeting (TPP2023), Tokyo Institute of Technology, 2023/10/30 
[2] 
Ayumu Saito and Reynald Affeldt.
A tentative formalization of a syntax for a probabilistic programming
language.
Mar 2023.
[ bib ]
Poster. 25th Workshop on Programming and Programming Languages (PPL2023), Nagoya University, 2023/03/0607 
[3] 
Reynald Affeldt and Cyril Cohen.
Formalization of integration theory in Coq.
Mar 2022.
[ bib ]
Poster. 24th Workshop on Programming and Programming Languages (PPL2022), 2022/03/08 
[4] 
Reynald Affeldt and Cyril Cohen.
Progress report on the formalization of the Lebesgue integral in
MathCompAnalysis.
Nov 2021.
[ bib ]
17th Theorem Proving and Provers Meeting (TPP2021), Kitami Institute of Technology, 2021/11/22 
[5] 
Ayumu Saito and Reynald Affeldt.
Extending Monae to formalize quicksort using monads in Coq.
Nov 2021.
[ bib ]
17th Theorem Proving and Provers Meeting (TPP2021), Kitami Institute of Technology, 2021/11/22 
[6] 
Reynald Affeldt and Cyril Cohen.
Formalization of measure theory in Coq.
Mar 2021.
[ bib ]
Poster. 23rd Workshop on Programming and Programming Languages (PPL2021), 2021/03/08 
[7] 
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue.
Future work towards a Coq library of succinct data structures.
Mar 2018.
[ bib ]
Poster. 20th Workshop on Programming and Programming Languages (PPL2018), Tottoriken, Yonagoshi, 2018/03/06 
[8] 
Reynald Affeldt.
Toward a library for information theory and errorcorrecting codes.
2017.
[ bib ]
13th Theorem Proving and Provers Meeting (TPP2017), Kyoto University, 2017/12/07, (in Japanese) 
[9] 
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue.
Safe lowlevel code generation in Coq using monomorphization and
monadification.
2017.
[ bib ]
The 114th Meeting of the IPSJ SIG on Programming (PRO114), Shizuokashi, 2017/06/09 
[10] 
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue.
Certified mon{omorphizadific}ation of Gallina for lowlevel
code extraction.
Mar 2017.
[ bib ]
Poster. 19th Workshop on Programming and Programming Languages (PPL2017), Yamanashiken, Fuefukishi, 2017/03/09 
[11] 
Reynald Affeldt.
Report on the Coq coding sprint.
Sep 2015.
[ bib ]
11th Theorem Proving and Provers Meeting (TPP2015), Kanagawa University, Shonan Hiratsuka campus, 2015/09/17, (in Japanese) 
[12] 
Reynald Affeldt and Kazuhiko Sakaguchi.
Demo of a Coq library for verification of C programs.
Mar 2014.
[ bib ]
Poster. 16th Workshop on Programming and Programming Languages (PPL2014), Kumamotoken, Asoshi, 2014/03/05, (in Japanese) 
[13] 
Reynald Affeldt and Kazuhiko Sakaguchi.
Presentation of a Coq library for formal verification of C
programs.
Nov 2013.
[ bib ]
9th Theorem Proving and Provers Meeting (TPP2013), Shinshu University, 2013/11/21, (in Japanese) pdf preprint 
[14] 
Reynald Affeldt and Kazuhiko Sakaguchi.
First building blocks for implementations of security protocols
verified in Coq.
Sep 2013.
[ bib ]
Poster. 30th Meeting of the Japan Society for Software Science and Technology, The University of Tokyo, Hongo campus, 2013/09/10 
[15] 
Reynald Affeldt, Manabu Hagiwara, and Jonas Sénizergues.
Formal verification of Shannon's theorems.
Nov 2012.
[ bib ]
8th Theorem Proving and Provers Meeting (TPP2012), Chiba University, 2012/11/21 
[16] 
Reynald Affeldt and Manabu Hagiwara.
Formalization of Shannon's theorems.
Mar 2012.
[ bib ]
Annual Spring Meeting of the Japan Society for Industrial and Applied Mathematics 2012, Kyushu University, 2012/03/08, (in Japanese) 
[17] 
Reynald Affeldt.
On construction of a library of formally verified lowlevel
arithmetic functions.
Nov 2011.
[ bib ]
7th Theorem Proving and Provers Meeting (TPP2011), National Institute of Advanced Industrial Science and Technology (AIST), Tsukuba Central, 2011/11/17 
[18] 
Reynald Affeldt and Kiyoshi Yamada.
Mechanical verification of C programs using separation logic.
Mar 2011.
[ bib ]
Poster. 13th Workshop on Programming and Programming Languages (PPL2011), Hokkaido, Sapporo, 2011/03/10 
[19] 
Reynald Affeldt.
Instrumenting errorcorrecting codes with SSReflect.
Nov 2010.
[ bib ]
6th Theorem Proving and Provers Meeting (TPP2010), Nagoya University, 2010/11/26 
[20] 
Reynald Affeldt.
A note about the formalization of errorcorrecting codes using
SSReflect.
Mar 2010.
[ bib ]
Annual Spring Meeting of the Japan Society for Industrial and Applied Mathematics 2010 (JSIAM Spring 2010), Tsukuba University, 2010/03/08, (in Japanese) slides 
[21] 
Reynald Affeldt, David Nowak, and Kiyoshi Yamada.
Certifying assembly with formal cryptographic proofs: the case of
BBS.
Nov 2009.
[ bib ]
5th Theorem Proving and Provers Meeting (TPP2009), Kwansei Gakuin University, 2009/11/21 
[22] 
Reynald Affeldt.
Verification in coq of an implementation of modular exponentiation
for an embedded system.
Mar 2009.
[ bib ]
Poster. 11th Workshop on Programming and Programming Languages (PPL2009), Gifuken, Takayamashi, 2009/03/09 poster file 
[23] 
Reynald Affeldt.
Verification of security protocols with a bounded number of sessions
based on resolution for rigid variables.
Nov 2008.
[ bib ]
4th Theorem Proving and Provers Meeting (TPP2008), Tohoko University, 2008/11/26 
[24] 
Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa.
Tools and experiments for formal verification of operating systems.
Mar 2006.
[ bib ]
Poster. 8th Workshop on Programming and Programming Languages (PPL2006), Shigaken, Ootsushi, 2006/03/05 
[25] 
Reynald Affeldt, Naoki Kobayashi, and Akinori Yonezawa.
Verification of concurrent programs using the Coq theorem prover: a
case study.
Jul 2004.
[ bib ]
Summer United Workshops on Parallel, Distributed and Cooperative Processing (SWoPP 2004), Aomori, 2004/07/30 
[1] 
Reynald Affeldt.
An Introduction to MathCompAnalysis.
2022.
[ bib ]
pdf preprint 
[2] 
Manabu Hagiwara and Reynald Affeldt.
Formal Proof using Coq/SSReflect/MathComp: Start
Formalization of Mathematics with Free Software.
Morikita Publishing, 2018.
[ bib ]
(in Japanese) publisher website and errata 
[3] 
Reynald Affeldt.
Introduction to Mathematical Components.
Computer Software, 34:6474, Apr 2017.
[ bib ]
(in Japanese) open access doi Japan Society for Software Science and Technology journal website 
[4] 
Reynald Affeldt.
Towards formal coding theory.
Chapter 15 of Evolving Theory of Errorcorrecting Codes, Manabu
Hagiwara (editor), pages 171189, Sep 2016.
[ bib ]
(in Japanese) Nippon Hyoronsha book website 
[5] 
Reynald Affeldt.
Formal verification using proofassistants: Recent results and
introduction to Coq.
Information Processing, 55:482491, May 2014.
[ bib ]
(in Japanese) open access Information Processing Society of Japan magazine website 
[6] 
Reynald Affeldt.
Towards formal coding theory.
Suugaku Seminaa (Mathematical Seminar), 618:7479, Apr 2013.
[ bib ]
(in Japanese) Nippon Hyoron sha co., Ltd journal website 
This file was generated by bibtex2html 1.99.