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

�Š‘®

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

Œ¤‹†ƒe�[ƒ}

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

˜_•¶

• 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.
  link
• ‹´–{‰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.