要旨
ラマヌジャンの公式$$ \frac{4}{\pi}=\sum_{n=0}^{\infty} \frac{(-1)^n (4n)! (1123+21460n)}{882^{2n+1}(4^n n!)^4} $$を用いて，円周率を計算するプログラムをHaskellで書きました． メモリ8GBのPCで動作させたところ，2000万桁程度まで実用的な速度で計算できました．
続きを読むOCaml標準ライブラリのList.sortを読む
この記事はML Advent Calendar 2017の10日目（！？）のために書かれました．
皆さんOCaml標準ライブラリのList.sortは使っていますか？
頻繁にリストに対してのソートを行うようならデータ構造かアルゴリズムを考え直した方が良いでしょうが，競プロの様にちょっとしたプログラムを書く時には僕もよくお世話になります．
マニュアルによると，そのList.sortはマージソートで実装されているようですが，僕のような者がちょっとやそっと工夫した程度では敵わないような最適化が施されています．今回はそのソースコードを読んでみましょう．
Coqによる型推論器の形式的検証
この記事は言語実装 Advent Calendar 2017の10日目（！？）のために書かれました． 9日目の記事は@ukitakaさんのSwiftコンパイラで採用されているパターンマッチの網羅性チェックの理論と実装です．
続きを読む最左最外簡約の性質をCoqで証明する
正規形を持つ項は最左最外簡約によってもその正規形に簡約されるのは有名な話． これはかなり嬉しくて，最左最外簡約は値呼びとは何だったのかと言わんばかりの優秀な評価戦略と言えるでしょう．
しかし，この性質は有名な割に定理証明支援系を使った証明を見ない気がします． みんな格好良い型の付いた言語に夢中なんでしょうか？ひとつCoqで証明してみましょう．
続きを読むTerm Rewriting and All Thatの練習問題をCoqで解く
この記事はTheorem Prover Advent Calendar 2016の8日目のために書かれました。
8日目の記事がまだ埋まっていないようなので、タイトルの通りTerm Rewriting and All Thatの練習問題で出てきた証明をいくつかCoqでやってみようと思います。
続きを読むCall-by-needを採用した言語のインタプリタの実装
この記事は言語実装 Advent Calendar 2016の9日目ために書かれました。
最近僕はcall-by-needに関連する研究をしており、気分を理解するためにcall-by-needを採用した言語のインタプリタをStandard MLで実装したりしました。今回はその時の事でも記事にしておきましょう。
続きを読む