Yoichi Hirai (平井洋一)


  • Computation and some logics
  • Becoming a "convenience logician" in the sense of "convenience stores"




formal verification of Ethereum Contracts

contact information

prizes, grants and distinctions

  • 科研費(研究活動スタート支援) 交付内定 2013--2015.
  • PPL2013 presentation award.
  • JSPS Research Fellowships for Young Scientists. 2011--2013.
  • Dean's Award of Graduate School of Information Science and Technology, The University of Tokyo,
    東京大学大学院 情報理工学系研究科 研究科長賞, 2010.
  • Classified among the 20 best candidates in Japanese Mathematical Olympiad. 2002.



  • Yoichi Hirai: Defining the Ethereum Virtual Machine for Interactive Theorem Provers (paper slides), 1st Workshop on Trusted Smart Contracts, 2017, accepted
  • Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews and Thomas Tuerk. Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor, FM 2016
  • Alessandro Facchini, Yoichi Hirai, Maarten Marx, and Evgeny Sherkhonov: Containment for conditional tree patterns. Logical Methods in Computer Science, 2015.
  • Yoichi Hirai, Reynald Affeldt: What can Coq do for Database Software? ---A Progress Report, JFLA 2014
  • Yoichi Hirai: Session Types in Abelian Logic, accepted to PLACES'13.
  • Yoichi Hirai: A Lambda Calculus for Gödel-Dummett Logic Capturing Waitfreedom, FLOPS 2012, LNCS 7294, pp. 151-165 (draft slide).
  • Kosuke Ono, Yoichi Hirai, Masami Hagiya, Natsuko Noda and Yoshinori Tanabe: Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications, SEFM'11, 2011.
  • Yoichi Hirai and Kazuhiko Yamamoto: Balancing Weight-Balanced Trees. Journal of Functional Programming, volume 21, issue 03, pp. 287-307. 2011. (project page, local PDF)
  • Yoichi Hirai: An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory. LPAR-16. 2010.
    paper (PDF) (The original version is available at www.springerlink.com)
  • 平井洋一「逐次一貫性下の知識伝達を表す直観主義様相論理」(PPL2010 カテゴリ1) 論文(pdf) スライド(pdf)


  • Yoichi Hirai: Duality between Nondeterminism and Concurrency on Generalized Petri Net, Bachelor's Thesis, 2008 (pdf).
  • Yoichi Hirai: An Intuitionistic Epistemic Logic for Asynchronous Communication, Master's Thesis, 2010 (pdf).
  • Yoichi Hirai: Hyper-Lambda Calculi, Doctoral Thesis, 2013 (pdf).


  • 平井洋一「分散プログラムを形式的証明から抽出する」 日本ソフトウェア科学会第26回大会で当日配布した修正版(pdf). (スライド(pdf))
  • 平井洋一「線形論理に基づく論理式=型=プロトコルの言語」(日本ソフトウェア科学会大会2008)


  • Yoichi Hirai: Morphing Smart Contracts with Bamboo (Cancun 2017-11-02) (slide)
  • Yoichi Hirai: Verifying Casper (Cancun 2017-11-01) (slides)
  • Yoichi Hirai: Specifying the Ethereum Virtual Machine for Theorem Provers (Cambridge 2017-09-13) (slides)
  • Yoichi Hirai: Isabelle/HOL on Fork Prevention in the Coming Ethereum Protocol (Berlin 2017-08-30) (slides)
  • Yoichi Hirai: Interactive theorem proving in the Ethereum project (Garching by Munich 2017-05-31) (slide)
  • Yoichi Hirai: Formal Verification for Ethereum (Amsterdam 2017-05-03) (slides video)
  • Yoichi Hirai: Blockchains: new home for proven-correct software (Paris 2017-02-17) (slide Video)
  • Yoichi Hirai: formal verification of smart contracts (Ethereum Meetup Berlin 2016-11-01).
  • 平井洋一: Formalizing Surreal Numbers and Combinatorial Games (第11回論理と計算セミナー)
  • 平井洋一「形式検証によるコマンド・インジェクション攻撃対策」 (日本応用数理学会2013年度年会 研究部会OS: 数理的技法による情報セキュリティ)
  • Session Types in Abelian Logic, PPL2013, 2013.
  • Hyper-Lambda Calculi, LOng Seminar, Oxford, 2013.
  • 提題「ゲーデル・ダメット論理における情報フロー」(科学基礎論学会2012年度講演会、学会特別企画ワークショップ「情報・時間・論理」), 東京都, 2012.
  • A. Facchini, Y. Hirai, M. Marx, E. Shekhernov: Containment for higher order tree patterns, FOX Closing Event, 2012.
  • Yoichi Hirai wants to be a traveling merchant at student session of OPLSS 2011.
  • Yoichi Hirai: Hyper-lambda calculus for waitfree computation: theory and implementation at ACAN workshop, 2011.
  • Yoichi Hirai: Determining the Valid Parameters for the Weight-Balanced Tree Algorithm at The 4th DIKU-IST Joint Workshop, 2011.
  • poster (Japanese) for an interview of DC2 fellowship of JSPS
  • Yoichi Hirai (speaker), Kazuhiko Yamamoto: Balance Condition on Weight-Balanced Trees at TPP'10
  • Yoichi Hirai: Disjunction Property and Finite Model Property For an Intuitionistic Epistemic Logic (NASSLLI2010 student session) (slide (pdf), paper).
  • 平井洋一「トートロジーの中で代入極小でない中間論理の公理」(PPL 2009, カテゴリ3)
  • 平井洋一「線形論理の証明としてメモリを書く」(CSCAT 2008) 口頭
  • 平井洋一「Prover-skeptic Dialogue for MALL」(SLACS2008)
  • 平井洋一「Generalizing Rationalizability in the Modal Mu-Calculus」
  • 平井洋一「論理学的にみたゲーム理論のプレイヤー」(東京財団VCASIインフォーマルセミナー)

teaching experiences

former positions


an ancient top page: piraspace

This page is powered by bootstrap framework.