Reynald Affeldt's Homepage

  アフェルト レナルド   阿费尔特 雷纳尔多

I am a senior research scientist (主任研究員) at AIST (National Institute of Advanced Industrial Science and Technology) (overview of AIST in 2017). I work^(*) in the Digital Architecture Research Center.

I can be reached by electronic-mail at reynald dot affeldt at aist dot go dot jp and by paper-mail at:

National Institute of Advanced Industrial Science and Technology (AIST),
Digital Architecture Research Center (DigiArc),
Annex 5th Floor, AIST Tokyo Waterfront, 2-4-7 Aomi, Koto-ku, Tokyo 135-0064 Japan /
  Cyber Physical Security Research Center (CPSEC),
  Central 1, 1-1-1 Umezono, Tsukuba, Ibaraki, 305-8560 Japan

I am mainly interested in formal verification of software using logic, and in particular the Coq proof-assistant.

Publications

• Current Coq projects:
• Analysis for MathComp
• Monadic Equational Reasoning
• 3D Geometry and Robotics
• Information Theory and Error-correcting codes

• Other verification projects:
• Verification of Low-level Programs
• Rigid resolution
• Applpi

• Teaching:
• A Coq/SSReflect/MathComp Tutorial
• An Introduction to Coq

• Organized events:
• The Coq Workshop 2019
• PRO101⁽²⁾
• PRO96⁽²⁾
• JSIAM-FAIS⁽¹⁾
• PRO91⁽²⁾
• TPP2011
• PRO86⁽²⁾
• Coq Café

(1) The Japan Society for Industrial and Applied Mathematics, Formal Approach to Information Security, 日本応用数理学会, 「数理的技法による情報セキュリティ」研究部会
(2) IPSJ Special Interest Group on Programming, 情報処理学会プログラミング研究発表会

(*) Previous affiliations in AIST: Software Quality Assurance Research Team in Cyber Physical Security Research Center (サイバーフィジカルセキュリティ研究センター, ソフトウェア品質保証研究チーム), Cyber Physical Architecture Research Group in ITRI (情報技術研究部門, サイバーフィジカルウェア研究グループ), Collaboration Promotion and International Affairs Division (産学官・国際連携推進部), Software Reliability Research Group in RISEC (セキュアシステム研究部門, 高信頼ソフトウェア研究グループ), Research Team for Software Security in RCIS (情報セキュリティ研究センター, ソフトウェアセキュリティ研究チーム).

I am a former student of the Yonezawa Laboratory (University of Tokyo, Graduate School of Information Science and Engineering, Department of Computer Science, 2001-2011---Graduate School of Science, Department of Information Science, until 2001) where I had the luck to work with Akinori Yonezawa, Naoki Kobayashi, Hidehiko Masuhara, and Eijiro Sumii.

TYPES Summer School '02 memo (including the scanned version of Per Martin-Löf's presentation).