Reynald Affeldt's Homepage

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

I am a chief senior research scientist (上級主任研究員) at AIST (National Institute of Advanced Industrial Science and Technology).

I work^(*) in the Digital Architecture Research Center.

I am also a visiting professor (客員教授) at NAIST (Nara Institute of Science and Technology): Formal verification laboratory / 形式検証研究室.

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

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
• Information Theory and Error-correcting codes
• 3D Geometry and Robotics

• Older 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).