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 (draftslide).
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