読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

定理証明器Isabelleで計算可能性の証明

Isabell 計算可能性 計算複雑性

偶然見つけました。
http://www2.score.cs.tsukuba.ac.jp/4eba3005-1/student/takuya-fujiwara-1/cs30bb30df30ca30fc767a88688cc76599-1/CSseminor2008_Fujiwara_Slides.pdf

将来、定理証明器で言語の開発をするようになるのかもしれない。

チューリング完全性とか後方互換性が証明されている言語とかあったらおもしろそう。