‹´–{ ‰pŽ÷ (Hideki Hashimoto)

�CŽm‰Û’ö

• “Œ‹ž‘åŠw‘åŠw‰@ �î•ñ—��HŠwŒ¤‹†‰È �”—��î•ñŠw�ê�U �CŽm‰Û’ö (2010”N3ŒŽ�C—¹)

Œ¤‹†ƒe�[ƒ}

• ’è—��Ø–¾Žx‰‡Œn (proof assistant) ‚ð—p‚¢‚½ƒvƒ�ƒOƒ‰ƒ€‰^ŽZ

˜_•¶

• ‹´–{‰pŽ÷. ’è—��Ø–¾Žx‰‡ŒnCoq‚ð—p‚¢‚½ƒvƒ�ƒOƒ‰ƒ€‰^ŽZ. �CŽm˜_•¶, �î•ñ—��HŠwŒnŒ¤‹†‰È�”—��î•ñŠw�ê�U, “Œ‹ž‘åŠw, 2010.
• Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, and Masato Takeichi. Program calculation in Coq. Research Report RR-2009-07, LIFO, University of Orléans, 2009.
  ƒvƒ�ƒWƒFƒNƒgƒy�[ƒW‚Ö
• ‹´–{‰pŽ÷, ŒÓ�U�], Julien Tesson, Frédéric Loulergue, •�Žs�³�l. ƒvƒ�ƒOƒ‰ƒ€‰^ŽZ‚Ì‚½‚ß ‚ÌCoqƒ‰ƒCƒuƒ‰ƒŠ. “ú–{ƒ\ƒtƒgƒEƒFƒA‰ÈŠw‰ï‘æ26‰ñ‘å‰ï—\�e�W, 2009.