以前から僕は単相の型推論アルゴリズムの健全性や完全性をCoqで検証していたのですが，最近*1let多相をサポートするように型推論器の実装と正当性の証明を修正したので記事にしておきましょう*2． *1:と言っても今年の1月ぐらいですが．本当はAdvent Calenda…

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

このエントリはML Advent Calendar 2015と言語実装 Advent Calendar 2015の20日目の記事です。 言語実装 Advent Calendar 2015の19日目の記事はh_sakuraiさんのJavaのサブセットコンパイラの作成でした。

現在僕は趣味でStandard MLのサブセットの処理系を実装しようとしているのですが、皆さんのご存知の通り、Standard MLの構文解析は非常に難しい事が知られています。 今回はML Kitの実装に関する文書を参考に構文解析器を実装した時の事について書きたいと思…

この記事はML Advent Calendar 2014 24日目のために書かれました。 Standard MLをはじめとするML系言語の始祖として、よくLCF MLの名前が挙げられます。 ここでは、LCF MLの言語機能について解説しつつ後の言語に与えた影響について思いを馳せたいと思います…

この記事はML Advent Calendar 2014 8日目のために書かれました。 多くの言語においてソートは標準ライブラリで提供されていますが、Standard ML Basis Libraryにはソートを行う関数が存在しません。 処理系依存で良ければSML/NJのListMergeSort.sortの様に…

大学でニュートン法とDKA法で方程式の解を求める課題が出たので、今回は趣向を変えてStandard MLで実装しました。

CoqにはExtractionという機能があり、Coqで書かれたソースコードから対応する他の言語のソースコードを出力する事ができます。今回はそのExtractionをStandard MLに対応させた事について書こうと思います。