‹´–{ ‰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‰ñ‘å‰ï—\eW, 2009.