Yoichi Hirai (平井洋一)

interests

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

resume

Logic Zoo Workshop 2013

DBLP

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.

publication

refereed

  • Yoichi Hirai, Reynald Affeldt: What can Coq do for Database Software? ---A Progress Report, accepted to 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: 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)

presentations

  • 平井洋一: 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

misc

an ancient top page: piraspace

This page is powered by bootstrap framework.