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

Isabell 計算可能性 計算複雑性

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

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

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