Ph.D. student
Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology
Cambridge, MA
The United States of America
Email: ikebuchi [at] mit.edu
Interests: Formal Verification, the Coq Proof Assistant, Term Rewriting System


Mirai Ikebuchi, "A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods", FSCD 2019, 24:1--24:17 (link) (received Best Paper Award by Junior Researchers)
Mirai Ikebuchi, Keisuke Nakano, "On Repetitive Right Application of B-Terms", FSCD 2018, 18:1-18:15 (link)


Jun.2019 : A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods, FSCD 2019
Jul.2018 : On repetitive right application of B terms (with Keisuke Nakano), FSCD 2018
Jul.2018 : ComplCoq: Rewrite Hint Construction with Completion Procedures (joint work with Keisuke Nakano), The Coq Workshop 2018
Mar.2017 : Bコンビネータの周期性について(On periodicity of B combinators), 19th Programming and Programming Language Workshop (won the poster award)
Feb.2017 : Word problems and a homological finiteness condition for monoids, 46th TRS meeting
Nov.2016 : Coqによる大規模データ処理・機械学習ライブラリの開発(Implementing a big data processing/machine learning library in Coq), 12th Theorem Proving and Provers (TPP 2016)

Coq Hacks

ComplCoq : Make your rewriting systems complete
Coq v8.8 with Set Printing Evars command : See below


Sep.2017- : Massachusetts Institute of Technology
Apr.2015-Mar.2017 : Master of Science, Nagoya University(Advisor: Hiroshi Ohta, Subadvisor: Jacques Garrigue)
Apr.2011-Mar.2015 : Bachelor of Science, Tsukuba University (valedictorian)


Apr.2015-Jan.2017 : Software Developer at IT Planning Inc.
Apr.2016-Aug.2016 : Research Internship at MIT CSAIL (PI: Adam Chlipala)
Mar.2011-Mar.2015 : Part-time Worker at IIJ Research Laboratory

Oct.2016-Feb.2017 : Teaching Assistant (Complex Analysis, G30 Program)
Sep.2016 : Committee Member in Program Committee for CUFP 2016
Apr.2014-Jul.2014 : Teaching Assistant (Exercise in Computer)