この記事はTheorem Prover Advent Calendar 2016の4日目のために書かれました。
少し季節外れの記事になりますが、前期はプロ演A[^1]の季節でしたね。
僕のTLでもC言語の課題に苦しめられた学部生のツイートが良く回ってきましたが、
とりわけ彼らが苦戦していたのはマージソートを書く課題のようでした。
面白そうなので僕もCoqで実装してみましょう。
もちろん、証明付きで。
この記事はTheorem Prover Advent Calendar 2016の4日目のために書かれました。
少し季節外れの記事になりますが、前期はプロ演A[^1]の季節でしたね。
僕のTLでもC言語の課題に苦しめられた学部生のツイートが良く回ってきましたが、
とりわけ彼らが苦戦していたのはマージソートを書く課題のようでした。
面白そうなので僕もCoqで実装してみましょう。
もちろん、証明付きで。
このエントリはML Advent Calendar 2015と言語実装 Advent Calendar 2015の20日目の記事です。 言語実装 Advent Calendar 2015の19日目の記事はh_sakuraiさんのJavaのサブセットコンパイラの作成でした。
続きを読むこのエントリはML Advent Calendar 2015の14日目の記事です。 13日目の記事はよんたさんの関数型プログラミングにおける再帰関数の考え方でした。
続きを読むこのエントリはTheorem Prover Advent Calendar 2015と言語実装 Advent Calendar 2015の11日目の記事です。 言語実装 Advent Calendar 2015の10日目の記事はkeenさんのリージョンについてでした。
続きを読むこの記事はML Advent Calendar8日目の記事として書かれました。 7日目の記事はでこれきさんのfoldみぎひだりです。
Standard MLやOCamlをはじめとしたML系の言語は関数型言語として有名ですが、参照、配列、例外といった副作用を伴う機能も扱う事ができます。 また、ML系の言語で手続き的に書いたからと言ってその言語の魅力が損なわれるわけではなく、 強い静的型付け、型推論やparametric polymorphismなどの恩恵を受けられるので、むしろ良く設計された手続き型言語のように映る事でしょう。 積極的にMLで手続き的な処理を書いていこうな。
続きを読む