interests
- Computation and some logics
- Becoming a "convenience logician" in the sense of "convenience stores"
resume
DBLP
github
contact information
prizes, grants and distinctions
-
科研費(研究活動スタート支援) 交付内定 2013--2015.
-
PPL2013 presentation award.
-
JSPS Research Fellowships for Young Scientists.
2011--2013.
- 平成21年度国家公務員採用Ⅰ種試験合格(名簿は有効期限切れ)
- 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.
publication
refereed
- 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)
slide
-
平井洋一「逐次一貫性下の知識伝達を表す直観主義様相論理」(PPL2010 カテゴリ1)
論文(pdf)
スライド(pdf)
theses
-
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).
unrefereed
-
平井洋一「分散プログラムを形式的証明から抽出する」
日本ソフトウェア科学会第26回大会で当日配布した修正版(pdf)．
(スライド(pdf))
- 平井洋一「線形論理に基づく論理式=型=プロトコルの言語」(日本ソフトウェア科学会大会2008)
talks
-
Yoichi Hirai: Blockchains as Kripke Models: an Analysis of Atomic Cross-Chain Swap (Limassol 2018-11-05) slide draft
-
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インフォーマルセミナー)
