|
[1]
|
石黒 吉洋 and Reynald Affeldt.
The Radon-Nikodým theorem and the Lebesgue-Stieltjes
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:1--28:27, 2023.
[ bib ]
doi arXiv: cs.LO 2209.02345
|
|
[3]
|
Reynald Affeldt, Jacques Garrigue, David Nowak, and 才川 隆文.
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 才川 隆文.
Reasoning with conditional probabilities and joint distributions in
Coq.
Computer
Software, 37(3):79--95, 2020.
[ bib ]
オープンアクセス doi pdf preprint プロジェクト ページ
|
|
[5]
|
Reynald Affeldt, Jacques Garrigue, and 才川 隆文.
A library for formalization of linear error-correcting codes.
Journal of
Automated Reasoning, 64:1123--1164, 2020.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[6]
|
Reynald Affeldt, Cyril Cohen, and Damien Rouhling.
Formalization techniques for asymptotic reasoning in classical
analysis.
Journal of Formalized Reasoning,
11(1):43--76, 2018.
[ bib ]
オープンアクセス doi プロジェクト ページ
|
|
[7]
|
田中 哲, Reynald Affeldt, and Jacques Garrigue.
Safe low-level code generation in Coq using monomorphization and
monadification.
Journal of Information
Processing, 26:54--72, 2018.
[ bib ]
Reprinted from IPSJ Transactions on Programming 10(6), 2017 オープンアクセス doi プロジェクト ページ
|
|
[8]
|
Reynald Affeldt and 坂口 和彦.
An intrinsic encoding of a subset of C and its application to TLS
network packet processing.
Journal of Formalized
Reasoning, 7(1):63--104, 2014.
[ bib ]
pdf preprint オープンアクセス doi プロジェクト ページ
|
|
[9]
|
Reynald Affeldt, 萩原 学, and Jonas Sénizergues.
Formalization of Shannon's theorems.
Journal of
Automated Reasoning, 53(1):63--103, 2014.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[10]
|
Reynald Affeldt.
On construction of a library of formally verified low-level
arithmetic functions.
Innovations in
Systems and Software Engineering, 9(2):59--77, 2013.
[ bib ]
NASA/Springer doi pdf preprint プロジェクト ページ
|
|
[11]
|
Reynald Affeldt, David Nowak, and 山田 聖.
Certifying assembly with formal security proofs: the case of BBS.
Science
of Computer Programming, 77(10--11):1058--1074, 2012.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[12]
|
Reynald Affeldt and Hubert Comon-Lundh.
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, State-of-the-Art Survey, pages 1--20. Springer,
May 2009.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[13]
|
Nicolas Marti and Reynald Affeldt.
A certified verifier for a fragment of separation logic.
Computer
Software, 25(3):135--147, 2008.
[ bib ]
Japan Society for Software Science and Technology. Iwanami Shoten オープンアクセス doi プロジェクト ページ Reprinted to Information and Media Technologies 4(2):304--316, 2009 doi pdf preprint
|
|
[14]
|
Reynald Affeldt, 小林 直樹, and 米澤 明憲.
Verification of concurrent programs using the Coq proof assistant:
a case study.
IPSJ Transactions on Programming, 46(SIG1(PRO24)):110--120,
2005.
[ bib ]
Information Processing Society of Japan. Reprinted to IPSJ Digital Courier 1:117--127, 2005 オープンアクセス doi pdf preprint プロジェクト ページ
|
|
[1]
|
Reynald Affeldt and 斉藤 歩夢.
Experimenting with an intrinsically-typed probabilistic programming
language in Coq.
In 21st Asian Symposium on Programming Languages and Systems
(APLAS 2023), Taipei,
Taiwan, November 26--29, 2023, volume 14405, pages 182--202. Springer, Nov
2023.
[ bib ]
doi pdf preprint
|
|
[2]
|
Reynald Affeldt, Cyril Cohen, and 斉藤 歩夢.
Semantics of probabilistic programs using s-finite kernels in Coq.
In 12th ACM SIGPLAN Conference on Certified Programs and Proofs
(CPP 2023), Boston, MA, USA,
January 16--17, 2023, pages 3--16. ACM Press, Jan 2023.
[ bib ]
doi オープンアクセス
|
|
[3]
|
斉藤 歩夢 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 26--28, 2022, volume 13544 of Lecture Notes in
Computer Science, pages 151--177. Springer, Sep 2022.
[ bib ]
pdf preprint doi プロジェクト ページ
|
|
[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:1--2:21.
Schloss Dagstuhl, Jun 2021.
[ bib ]
doi Post-Proceedings. arXiv preprint cs.LO 2011.03463
|
|
[5]
|
Reynald Affeldt, Jacques Garrigue, and 才川 隆文.
Formal adventures in convex and conical spaces.
In 13th Conference on Intelligent Computer Mathematics
(CICM 2020), Bertinoro, Forli,
Italy, July 26--31, 2020, volume 12236 of Lecture Notes in Artificial
Intelligence, pages 23--38. Springer, Jul 2020.
[ bib ]
doi オープンアクセス
|
|
[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 29--July 6,
2020, volume 12167 of Lecture Notes in Artificial Intelligence, pages
3--20. Springer, Jul 2020.
[ bib ]
doi オープンアクセス
|
|
[7]
|
Reynald Affeldt, David Nowak, and 才川 隆文.
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 7--9, 2019, volume 11825 of Lecture Notes in
Computer Science, pages 226--254. Springer, Oct 2019.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[8]
|
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and 田中 一成.
Proving tree algorithms for succinct data structures.
In 10th International Conference on Interactive Theorem Proving
(ITP 2019), Portland, OR, USA, September
8-13, 2019, volume 141 of Leibniz International Proceedings in
Informatics, pages 28:1--28:19. Schloss Dagstuhl, Sep 2019.
[ bib ]
オープンアクセス doi pdf preprint プロジェクト ページ
|
|
[9]
|
Reynald Affeldt, Jacques Garrigue, and 才川 隆文.
Examples of formal proofs about data compression.
In International Symposium on Information Theory and Its
Applications (ISITA 2018),
Singapore, October 28--31, 2018, pages 633--637. IEEE, Oct 2018.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[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
16--17, 2017, pages 30--42. ACM Press, Jan 2017.
[ bib ]
doi pdf preprint プロジェクト ページ スライド
|
|
[11]
|
田中 哲, 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 14--18, 2016, volume 10009 of
Lecture Notes in Computer Science, pages 243--260. Springer, Nov 2016.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[12]
|
Reynald Affeldt, Jacques Garrigue, and 才川 隆文.
Formalization of Reed-Solomon codes and progress report on
formalization of LDPC codes.
In International Symposium on Information Theory and Its
Applications (ISITA 2016),
Monterey, California, USA, October 30--November 2, 2016, pages 537--541.
IEICE. IEEE Xplore, Oct 2016.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[13]
|
Reynald Affeldt and Jacques Garrigue.
Formalization of error-correcting codes: from Hamming to modern
coding theory.
In 6th Conference on Interactive Theorem Proving
(ITP 2015), Nanjing,
China, August 24--27, 2015, volume 9236 of Lecture Notes in Computer
Science, pages 17--33. Springer, Aug 2015.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[14]
|
小尾 良介, 萩原 学, and Reynald Affeldt.
Formalization of variable-length source coding theorem: Direct part.
In International Symposium on Information Theory and Its
Applications (ISITA 2014), Melbourne, Australia, October 26--29, 2014, pages
201--205. 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 35--46. ACM Press, Jan 2013.
[ bib ]
doi pdf preprint
|
|
[16]
|
Reynald Affeldt and 萩原 学.
Formalization of Shannon's theorems in SSReflect-Coq.
In 3rd Conference on Interactive Theorem Proving
(ITP 2012), Princeton, New Jersey,
USA, August 13--15, 2012, volume 7406 of Lecture Notes in Computer
Science, pages 233--249. Springer, Aug 2012.
[ bib ]
doi pdf preprint プロジェクト ページ スライド
|
|
[17]
|
Reynald Affeldt.
On construction of a library of formally verified low-level
arithmetic functions.
In 27th ACM SIGAPP Symposium On Applied Computing
(SAC 2012), Riva del Garda
(Trento), Italy, March 26--30, 2012, volume 2, pages 1326--1331. ACM Press,
Mar 2012.
[ bib ]
pdf preprint doi Software Verification and Testing Track プロジェクト ページ
|
|
[18]
|
Reynald Affeldt, David Nowak, and 大岩 寛.
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
27--36. ACM Press, Jan 2012.
[ bib ]
pdf preprint doi
|
|
[19]
|
Reynald Affeldt, David Nowak, and 山田 聖.
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 プロジェクト ページ Proceedings of the 9th International Workshop on Automated Verification of Critical Systems (AVoCS 2009), Swansea University Computer Science, September 23--25, 2009. Preliminary version: Technical Report of Computer Science, Swansea University CSR-2-2009
|
|
[20]
|
Reynald Affeldt and Hubert Comon-Lundh.
A note on first-order 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
(FCS-ARSPA-WITS
2008), Pittsburgh, PA, USA, June 21--22, 2008, pages 11--20, Jun 2008.
[ bib ]
pdf preprint プロジェクト ページ
|
|
[21]
|
Reynald Affeldt, 田中 三貴, and Nicolas Marti.
Formal proof of provable security by game-playing in a proof
assistant.
In 1st International Conference on Provable Security (Provsec
2007), Wollongong, NSW, Australia, November 1--2, 2007, volume 4784 of
Lecture Notes in Computer Science, pages 151--168. 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 6--8,
2006, volume 4435 of Lecture Notes in Computer Science, pages
346--360. Springer, Jan 2008.
[ bib ]
doi pdf preprint プロジェクト ページ
|
|
[23]
|
Nicolas Marti, Reynald Affeldt, and 米澤 明憲.
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 29--November 3, 2006, volume 4260 of
Lecture Notes in Computer Science, pages 400--419. Springer, Oct 2006.
[ bib ]
doi pdf preprint
|
|
[24]
|
Reynald Affeldt and 小林 直樹.
Partial order reduction for verification of spatial properties of
pi-calculus processes.
Electronic Notes in Theoretical Computer Science,
128(2):151--168, 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 小林 直樹.
A Coq library for verification of concurrent programs.
Electronic Notes in Theoretical Computer Science, 199:17--32,
Feb 2008.
[ bib ]
doi pdf preprint プロジェクト ページ Elsevier. Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFM 2004), Cork, Ireland, July 5, 2004
|
|
[26]
|
Reynald Affeldt and 小林 直樹.
Formalization and verification of a mail server in Coq.
In International Symposium on Software Security, Tokyo, Japan,
November 8--10, 2002, volume 2609 of Lecture Notes in Computer Science,
Hot Topics, pages 217--233. Springer, Feb 2003.
[ bib ]
doi pdf preprint スライド
|
|
[27]
|
Reynald Affeldt, 増原 英彦, 住井 英二郎, and 米澤 明憲.
Supporting objects in run-time bytecode specialization.
In ACM SIGPLAN Asian Symposium on Partial Evaluation and
Semantics-based Program Manipulation (ASIA-PEPM 2002), Aizu, Japan, September
12--14, 2002, pages 50--60. ACM Press, Sep 2002.
[ bib ]
doi pdf preprint スライド
|
|
[1]
|
斉藤 歩夢 and Reynald Affeldt.
An intrinsically-typed probabilistic programming language in Coq
(extended abstract).
The Workshop on Type-Driven Development (TyDe 2023), Seattle,
Washington, United States, September 4, 2023, Sep 2023.
[ bib ]
pdf preprint オープンアクセス
|
|
[2]
|
Reynald Affeldt, Jacques Garrigue, and 才川 隆文.
Environment-friendly monadic equational reasoning for OCaml.
The Coq Workshop 2023, Białystok, Poland, July 31, 2023, Jul 2023.
[ bib ]
pdf preprint プロジェクト ページ オープンアクセス
|
|
[3]
|
Reynald Affeldt and Cyril Cohen.
Formalization of the Lebesgue measure in MathComp-Analysis.
The Coq Workshop 2021, online, July 2, 2021, Jul 2021.
[ bib ]
pdf preprint プロジェクト ページ オープンアクセス
|
|
[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 ]
オープンアクセス
|
|
[5]
|
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and 田中 一成.
Experience report: Type-driven development of certified tree
algorithms in Coq.
The Coq Workshop 2019, Portland, OR, USA, September 8, 2019, Sep
2019.
[ bib ]
オープンアクセス
|
|
[6]
|
Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling, and Pierre-Yves
Strub.
Classical analysis with Coq.
The Coq Workshop 2018, Oxford, UK, July 8, 2018, Jul 2018.
[ bib ]
プロジェクト ページ pdf preprint
|
|
[7]
|
Reynald Affeldt and Jacques Garrigue.
Formalization of error-correcting codes using SSReflect.
The 6th Coq Workshop, Vienna, Austria, July 7, 2014, Jul 2014.
[ bib ]
プロジェクト ページ
|
|
[8]
|
Reynald Affeldt and 坂口 和彦.
First building blocks for implementations of security protocols
verified in Coq.
The 5th Coq Workshop, Rennes, France, July 22, 2013, Jul 2013.
[ bib ]
プロジェクト ページ
|
|
[9]
|
Nicolas Marti, Reynald Affeldt, and 米澤 明憲.
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 61--72 スライド プロジェクト ページ
|
|
[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), Saint-Jacut-de-la-Mer, France, January 30--February 2, pages
300--304. Inria and others, Jan 2024.
[ bib ]
オープンアクセス
|
|
[2]
|
石黒 吉洋 and Reynald Affeldt.
A progress report on formalization of measure theory with
MathComp-Analysis.
In 第25
回プログラミングおよびプログラミング言語ワークショップ(PPL2023),
名古屋大学, March 6--8, 2023, Mar 2023.
[ bib ]
15 pages. pdf preprint conference website
|
|
[3]
|
斉藤 歩夢 and Reynald Affeldt.
Practical aspects of monadic equational reasoning in Coq.
In 第24
回プログラミングおよびプログラミング言語ワークショップ(PPL2022),
March 6--8, 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 29--February 1, pages 23--30. CEA List and
others, Jan 2020.
[ bib ]
pdf preprint オープンアクセス
|
|
[5]
|
Reynald Affeldt, Jacques Garrigue, and 才川 隆文.
Reasoning with conditional probabilities and joint distributions in
Coq.
In 第21
回プログラミングおよびプログラミング言語ワークショップ(PPL2019),
岩手県花巻市, March 6--8, 2019, Mar 2019.
[ bib ]
16 pages. pdf preprint conference website
|
|
[6]
|
田中 哲, Reynald Affeldt, and Jacques Garrigue.
Formal verification of the rank function for succinct data
structures.
In 第18
回プログラミングおよびプログラミング言語ワークショップ(PPL2016),
岡山県玉野市, March 7--9, 2016, Mar 2016.
[ bib ]
15 pages. 論文賞 conference website プロジェクト ページ
|
|
[7]
|
平井 洋一 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 8--11, pages 33--48, Jan 2014.
[ bib ]
|
|
[8]
|
Reynald Affeldt.
Toward formal construction of assembly arithmetic functions from
pseudo-code.
In 第12
回プログラミングおよびプログラミング言語ワークショップ(PPL2010),
香川県琴平温泉, March 3--5, 2010, pages 1--14, Mar 2010.
[ bib ]
pdf preprint conference website プロジェクト ページ
|
|
[9]
|
Nicolas Marti and Reynald Affeldt.
A certified verifier for a fragment of separation logic.
In 第9
回プログラミングおよびプログラミング言語ワークショップ(PPL2007),
石川県加賀市, March 8--10, 2007, pages 187--199, Mar 2007.
[ bib ]
論文賞 プロジェクト ページ
|
|
[1]
|
Reynald Affeldt and David Nowak.
Experimenting with monadic equational reasoning in Coq.
In 日本ソフトウェア科学会 第35 回大会
講演論文集 (JSSST 2018),
大阪府吹田市, August 29--31, 2018, Aug 2018.
[ bib ]
14 pages プロジェクト ページ 日本語でのタイトル: CoqにおけるMonadic等式推論の実験 pdf preprint
|
|
[2]
|
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and 田中 一成.
Proving tree algorithms for succinct data structures.
In 日本ソフトウェア科学会 第35 回大会
講演論文集 (JSSST 2018),
大阪府吹田市, August 29--31, 2018, Aug 2018.
[ bib ]
13 pages プロジェクト ページ 日本語でのタイトル: 簡潔データ構造における木構造アルゴリズムの形式証明について pdf preprint
|
|
[3]
|
田中 哲, Reynald Affeldt, and Jacques Garrigue.
Coq用Cコード生成器の線形性検査拡張.
In 日本ソフトウェア科学会 第35 回大会
講演論文集 (JSSST 2018),
大阪府吹田市, August 29--31, 2018, Aug 2018.
[ bib ]
11 pages (日本語) 日本語でのタイトル: Coq用Cコード生成器の線形性検査拡張 pdf preprint
|
|
[4]
|
Reynald Affeldt and Cyril Cohen.
Formal foundations for rigid body transformation.
In 日本ソフトウェア科学会 第33 回大会
講演論文集 (JSSST 2016),
宮城県仙台市, September 6--9, 2016, Sep 2016.
[ bib ]
11 pages プロジェクト ページ 日本語でのタイトル: 剛体変換のための形式基礎 pdf preprint
|
|
[5]
|
Reynald Affeldt.
An intrinsic encoding of a subset of C and its application to TLS
network packet processing.
In 日本応用数理学会 2015 年度年会 講演予稿集,
金沢大学, 角間キャンパス, September 9-11, 2015, pages 306--307,
Sep 2015.
[ bib ]
プロジェクト ページ pdf preprint
|
|
[6]
|
Reynald Affeldt and Jacques Garrigue.
Formalization of error-correcting codes using SSReflect.
In MI Lecture Note 研究集会
高信頼な理論と実装のための定理証明および定理証明器
(TPP2014), 九州大学, December 3--5, 2014, volume 61, pages 76--78, Dec
2014.
[ bib ]
プロジェクト ページ
|
|
[7]
|
Reynald Affeldt.
Formalization of Shannon's theorems using the Coq
proof-assistant.
In 2013年電子情報通信学会ソサイエティ大会
基礎・境界 講演論文集, 福岡工業大学, September 17--20, 2013,
pages 39--44, Sep 2013.
[ bib ]
pdf preprint プロジェクト ページ conference website IEICE, Technical Committee on Information Theory
|
|
[8]
|
Reynald Affeldt.
About the formal verification of Shannon's theorems.
In COE Lecture Note 九州大学
マス・フォア・インダストリ研究所,
共同利用研究集会II:モダン符号理論からポストモダン符号理論への展望,
九州大学, March 4--7, 2013, volume 44, pages 86--94, Mar 2013.
[ bib ]
pdf preprint プロジェクト ページ
|
|
[9]
|
Reynald Affeldt.
Toward a library of verified arithmetic functions.
In 日本応用数理学会 2011 年度年会 講演予稿集,
同志社大学, September 14--16, 2011, pages 377--378, Sep 2011.
[ bib ]
プロジェクト ページ
|
|
[10]
|
Reynald Affeldt and 山田 聖.
Formal verification of C programs for implementations of
communication protocols.
In 日本ソフトウェア科学会 第28 回大会
講演論文集 (JSSST 2011),
沖縄県那覇市, September 26--29, 2011, Sep 2011.
[ bib ]
pdf preprint プロジェクト ページ
|
|
[11]
|
Reynald Affeldt, David Nowak, and 山田 聖.
形式的な暗号学的安全性証明によるアセンブリプログラムの安全性検証：bbsの事例.
In 日本応用数理学会 2009 年度年会 講演予稿集
(JSIAM 2009),
大阪大学, September 28--30, 2009, pages 53--54, Sep 2009.
[ bib ]
pdf preprint スライド (日本語) プロジェクト ページ
|
|
[12]
|
Reynald Affeldt and Hubert Comon-Lundh.
Towards verification with no false attack of security protocols in
first-order logic.
In 日本応用数理学会 2008 年度年会 講演予稿集
(JSIAM 2008),
東京大学, 柏キャンパス, September 17--19, 2008, pages 177--178,
Sep 2008.
[ bib ]
pdf preprint スライド プロジェクト ページ
|
|
[13]
|
Reynald Affeldt and 川本 裕輔.
Report on FCS-ARSPA-WITS, CSF, FCC'08---about automated
verification and certification.
In 日本応用数理学会 2008 年度年会 講演予稿集,
東京大学, 柏キャンパス, September 17--19, 2008, pages 187--188,
Sep 2008.
[ bib ]
日本語でのタイトル: FCS-ARSPA-WITS, CSF, FCC'08参加報告---自動検証と形式的証明について
|
|
[14]
|
川本 裕輔 and Reynald Affeldt.
FCS-ARSPA-WITS, CSF,
FCC'08参加報告---安全性の形式化について.
In 日本応用数理学会 2008 年度年会 講演予稿集,
東京大学, 柏キャンパス, September 17--19, 2008, pages 185--186,
Sep 2008.
[ bib ]
(日本語)
|
|
[15]
|
Reynald Affeldt, 田中 三貴, and Nicolas Marti.
証明可能安全性の形式的証明:定理証明ツールによるゲームの手法.
In 日本応用数理学会 2017 年度年会 講演予稿集
(JSIAM 2007),
北海道大学, September 15--17, 2007, pages 44--45, Sep 2007.
[ bib ]
pdf preprint (日本語)
|
|
[16]
|
Reynald Affeldt and Nicolas Marti.
Formal verification of arithmetic functions in SmartMIPS assembly.
In 日本ソフトウェア科学会 第23 回大会
講演論文集, 東京大学, 本郷キャンパス, September 13--15,
2006, Sep 2006.
[ bib ]
pdf preprint プロジェクト ページ
|
|
[17]
|
Nicolas Marti, Reynald Affeldt, and 米澤 明憲.
Model-checking of a multi-threaded operating system.
In 日本ソフトウェア科学会 第23 回大会
講演論文集, 東京大学, 本郷キャンパス, September 13--15,
2006, Sep 2006.
[ bib ]
pdf preprint プロジェクト ページ
|
|
[18]
|
Nicolas Marti, Reynald Affeldt, and 米澤 明憲.
Towards formal verification of memory properties using separation
logic.
In 日本ソフトウェア科学会 第22 回大会
講演論文集, 東北大学, 青葉山キャンパス, September 13--15,
2005, Sep 2005.
[ bib ]
pdf preprint スライド プロジェクト ページ
|
|
[19]
|
Reynald Affeldt, 増原 英彦, 住井 英二郎, and 米澤 明憲.
Supporting objects in run-time bytecode specialization.
In 日本ソフトウェア科学会 第18 回大会
講演論文集 (JSSST
2011), 公立はこだて未来大学, September 18--20, 2001, Sep 2001.
[ bib ]
pdf preprint
|
|
[1]
|
Reynald Affeldt and Zachary Stone.
The fundamental theorem of calculus for the Lebesgue integral in
MathComp-Analysis.
Oct 2023.
[ bib ]
第19 回定理証明及び定理証明系ミーティング (TPP2023), 東京工業大学, 2023/10/30
|
|
[2]
|
斉藤 歩夢 and Reynald Affeldt.
確率的プログラミング言語の形式基盤を構文で拡張する試み.
Mar 2023.
[ bib ]
ポスター. 第25 回プログラミングおよびプログラミング言語ワークショップ(PPL2023), 名古屋大学, 2023/03/06-07
|
|
[3]
|
Reynald Affeldt and Cyril Cohen.
Formalization of integration theory in Coq.
Mar 2022.
[ bib ]
ポスター. 第24 回プログラミングおよびプログラミング言語ワークショップ(PPL2022), 2022/03/08
|
|
[4]
|
Reynald Affeldt and Cyril Cohen.
Progress report on the formalization of the Lebesgue integral in
MathComp-Analysis.
Nov 2021.
[ bib ]
第17 回定理証明及び定理証明系ミーティング (TPP2021), 北見工業大学, 2021/11/22
|
|
[5]
|
斉藤 歩夢 and Reynald Affeldt.
定理証明支援系Coqでのモナドを用いたクイックソートの形式化とMonaeの拡張.
Nov 2021.
[ bib ]
第17 回定理証明及び定理証明系ミーティング (TPP2021), 北見工業大学, 2021/11/22
|
|
[6]
|
Reynald Affeldt and Cyril Cohen.
Formalization of measure theory in Coq.
Mar 2021.
[ bib ]
ポスター. 第23 回プログラミングおよびプログラミング言語ワークショップ(PPL2021), 2021/03/08
|
|
[7]
|
田中 哲, Reynald Affeldt, and Jacques Garrigue.
Coqによる簡潔データ構造のライブラリに向けての今後の課題.
Mar 2018.
[ bib ]
ポスター. 第20 回プログラミングおよびプログラミング言語ワークショップ(PPL2018), 鳥取県米子市, 2018/03/06
|
|
[8]
|
Reynald Affeldt.
形式的な情報・符号理論のライブラリに向けて.
2017.
[ bib ]
第13 回定理証明及び定理証明系ミーティング (TPP2017), 京都大学, 2017/12/07, (日本語)
|
|
[9]
|
田中 哲, Reynald Affeldt, and Jacques Garrigue.
Safe low-level code generation in Coq using monomorphization and
monadification.
2017.
[ bib ]
第114 回プログラミング研究発表会 情報処理学会プログラミング研究会, 静岡市, 2017/06/09
|
|
[10]
|
田中 哲, Reynald Affeldt, and Jacques Garrigue.
Certified mon{omorphiz|adific}ation of Gallina for low-level
code extraction.
Mar 2017.
[ bib ]
ポスター. 第19 回プログラミングおよびプログラミング言語ワークショップ(PPL2017), 山梨県笛吹市, 2017/03/09
|
|
[11]
|
Reynald Affeldt.
Coq coding sprint参加報告.
Sep 2015.
[ bib ]
第11 回定理証明及び定理証明系ミーティング (TPP2015), 神奈川大学, 湘南ひらつかキャンパス, 2015/09/17, (日本語)
|
|
[12]
|
Reynald Affeldt and 坂口 和彦.
CoqによるCプログラムの検証基盤のデモ.
Mar 2014.
[ bib ]
ポスター. 第16 回プログラミングおよびプログラミング言語ワークショップ(PPL2014), 熊本県阿蘇市, 2014/03/05, (日本語)
|
|
[13]
|
Reynald Affeldt and 坂口 和彦.
C言語プログラムの形式検証のためのCoqライブラリの紹介.
Nov 2013.
[ bib ]
第9 回定理証明及び定理証明系ミーティング (TPP2013), 信州大学, 2013/11/21, (日本語) pdf preprint
|
|
[14]
|
Reynald Affeldt and 坂口 和彦.
First building blocks for implementations of security protocols
verified in Coq.
Sep 2013.
[ bib ]
ポスター. 日本ソフトウェア科学会 第30 回大会, 東京大学, 本郷キャンパス, 2013/09/10
|
|
[15]
|
Reynald Affeldt, 萩原 学, and Jonas Sénizergues.
Formal verification of Shannon's theorems.
Nov 2012.
[ bib ]
第8 回定理証明及び定理証明系ミーティング (TPP2012), 千葉大学, 2012/11/21
|
|
[16]
|
Reynald Affeldt and 萩原 学.
シャノンの定理の形式化.
Mar 2012.
[ bib ]
日本応用数理学会 2012 年春の研究部会連合発表会, 九州大学, 2012/03/08, (日本語)
|
|
[17]
|
Reynald Affeldt.
On construction of a library of formally verified low-level
arithmetic functions.
Nov 2011.
[ bib ]
第7 回定理証明及び定理証明系ミーティング (TPP2011), 産業技術総合研究所 (AIST), つくば中央, 2011/11/17
|
|
[18]
|
Reynald Affeldt and 山田 聖.
分離論理を用いた，C言語プログラムの機械的検証.
Mar 2011.
[ bib ]
ポスター. 第13 回プログラミングおよびプログラミング言語ワークショップ(PPL2011), 北海道札幌市, 2011/03/10
|
|
[19]
|
Reynald Affeldt.
Instrumenting error-correcting codes with SSReflect.
Nov 2010.
[ bib ]
第6 回定理証明及び定理証明系ミーティング (TPP2010), 名古屋大学, 2010/11/26
|
|
[20]
|
Reynald Affeldt.
SSReflectに よる符号理論の形式化に関する一考察.
Mar 2010.
[ bib ]
日本応用数理学会 2010 年春の研究部会連合発表会 (JSIAM Spring 2010), 筑波大学, 2010/03/08, (日本語) スライド
|
|
[21]
|
Reynald Affeldt, David Nowak, and 山田 聖.
Certifying assembly with formal cryptographic proofs: the case of
BBS.
Nov 2009.
[ bib ]
第5 回定理証明及び定理証明系ミーティング (TPP2009), 関西学院大学, 2009/11/21
|
|
[22]
|
Reynald Affeldt.
Coq上 での組込み用途の冪剰余の検証.
Mar 2009.
[ bib ]
ポスター. 第11 回プログラミングおよびプログラミング言語ワークショップ(PPL2009), 岐阜県高山市, 2009/03/09 ポスター ファイル
|
|
[23]
|
Reynald Affeldt.
Verification of security protocols with a bounded number of sessions
based on resolution for rigid variables.
Nov 2008.
[ bib ]
第4 回定理証明及び定理証明系ミーティング (TPP2008), 東北大学, 2008/11/26
|
|
[24]
|
Nicolas Marti, Reynald Affeldt, and 米澤 明憲.
Tools and experiments for formal verification of operating systems.
Mar 2006.
[ bib ]
ポスター. 第8 回プログラミングおよびプログラミング言語ワークショップ(PPL2006), 滋賀県大津市, 2006/03/05
|
|
[25]
|
Reynald Affeldt, 小林 直樹, and 米澤 明憲.
Verification of concurrent programs using the Coq theorem prover: a
case study.
Jul 2004.
[ bib ]
並列/分散/協調処理に関するサマー・ワークショップ(SWoPP 2004), 青森, 2004/07/30
|