この記事はTheorem Prover Advent Calendar 2016の8日目のために書かれました。 8日目の記事がまだ埋まっていないようなので、タイトルの通りTerm Rewriting and All Thatの練習問題で出てきた証明をいくつかCoqでやってみようと思います。

この記事は言語実装 Advent Calendar 2016の9日目ために書かれました。 最近僕はcall-by-needに関連する研究をしており、気分を理解するためにcall-by-needを採用した言語のインタプリタをStandard MLで実装したりしました。今回はその時の事でも記事にして…

この記事は言語実装 Advent Calendar 2016のために書かれました。 元々僕はStandard MLで一からコンパイラを書こうとしていたんですが、ローレベルあんまり詳しくなくてネイティブコードを生成できるようにするのが面倒だったのと、Standard MLのsyntax suga…

この記事はTheorem Prover Advent Calendar 2016の4日目のために書かれました。 少し季節外れの記事になりますが、前期はプロ演A[^1]の季節でしたね。 僕のTLでもC言語の課題に苦しめられた学部生のツイートが良く回ってきましたが、 とりわけ彼らが苦戦して…

二分探索は言わずと知れた探索アルゴリズムですが、 実際に実装しようとすると無限ループしたり正しい答えが得られなかったりする事も多いのではないでしょうか。 そこで、ここではCoqで二分探索を実装し、正当性の証明を行いました。

最近研究でCoqぐらいしか書いてないので、リハビリがてらAtCoderで 開かれるコンテストにOCamlで参加して遊んでます。 僕は個人的な趣味もあってOCamlを使う際は専ら言語処理系を書いていましたが、 競技プログラミングでは全く関係ない題材を扱う必要がある…