fetburner.core

コアダンプ

2020-12-01から1ヶ月間の記事一覧

List.fold_right で List.fold_left を書く

この記事は ML Advent Calendar 2020 の14日目の記事です. リストの Church encoding と言えば List.fold_right で表現することが多いように思いますが,果たして List.fold_right だけしか使わずに様々なリストについての再帰関数を表現できるのか疑問に思…

ML のサブセットの型推論器を Coq で検証する

この記事は言語実装 Advent Calendar 2020 の5日目の記事です. 一度でも型推論器を書いたことがあれば,そのあまりの邪悪さ,あるいはその複雑さに恐れ慄いたことでしょう. 参照を用いて単一化を実現しようものなら構文木は参照に汚染され,純粋関数型に実…

効率的な正規表現エンジンを Coq で検証する

今年はそれらしきアドベントカレンダーが無いので,この記事は ML アドベントカレンダー 2020 の4日目の記事と言い張ってみます. ML って本を正せば定理証明支援系由来ですし.最後にちょっと OCaml を使ってますし. Coq によって検証された正規表現エンジ…