An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory. - Yoichi Hirai (LPAR (Dakar), 2010)

Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications. - Kosuke Ono; Yoichi Hirai; Yoshinori Tanabe; Natsuko Noda; Masami Hagiya (SEFM, 2011)

Balancing weight-balanced trees. - Yoichi Hirai; Kazuhiko Yamamoto (J. Funct. Program., 2011)

A Lambda Calculus for Gödel-Dummett Logic Capturing Waitfreedom. - Yoichi Hirai (FLOPS, 2012)

Session Types in Abelian Logic. - Yoichi Hirai (PLACES, 2013)

What could Coq do for Database Software? - A Progress Report. - Yoichi Hirai; Reynald Affeldt (JFLA, 2014)

Containment for Conditional Tree Patterns. - Alessandro Facchini; Yoichi Hirai; Maarten Marx; Evgeny Sherkhonov (Log. Methods Comput. Sci., 2015)

Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor. - Hanno Becker; Juan Manuel Crespo; Jacek Galowicz; Ulrich Hensel; Yoichi Hirai; César Kunz; Keiko Nakata 001; Jorge Luis Sacchini; Hendrik Tews; Thomas Tuerk (FM, 2016)

Defining the Ethereum Virtual Machine for Interactive Theorem Provers. - Yoichi Hirai (Financial Cryptography Workshops, 2017)

Blockchains as Kripke Models: An Analysis of Atomic Cross-Chain Swap. - Yoichi Hirai (ISoLA (4), 2018)

Developing With Formal Methods at BedRock Systems, Inc. - Gregory Malecha; Gordon Stewart 001; Frantisek Farka; Jasper Haag; Yoichi Hirai (IEEE Secur. Priv., 2022)