読者です 読者をやめる 読者になる 読者になる

チラシの裏

プログラミングとか色々

OCaml

MinCamlに簡単な最適化を追加する

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

二分探索に証明を付ける

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

OCamlで車輪を再発明する

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

GADTを用いた二項ヒープの実装

このエントリはML Advent Calendar 2015の14日目の記事です。 13日目の記事はよんたさんの関数型プログラミングにおける再帰関数の考え方でした。

型推論の健全性の証明

このエントリはTheorem Prover Advent Calendar 2015と言語実装 Advent Calendar 2015の11日目の記事です。 言語実装 Advent Calendar 2015の10日目の記事はkeenさんのリージョンについてでした。

手続き型言語OCaml

この記事はML Advent Calendar8日目の記事として書かれました。 7日目の記事はでこれきさんのfoldみぎひだりです。 Standard MLやOCamlをはじめとしたML系の言語は関数型言語として有名ですが、参照、配列、例外といった副作用を伴う機能も扱う事ができます…

LCF MLについて

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

ちょっとだけクイックソート

よい実装かどうかは抜きにして、一般的な関数型言語ではリストに対するクイックソートを簡単に書く事ができます。 一方、そのようなよく見かける実装ではリストの結合を再帰内で用いていますが、 一般に関数型言語ではの時間計算量を要するため、リストの結…

CoqからSMLへ

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

ガウスの消去法

学校の課題でガウスの消去法を実装しました。言語は特に指定されなかったのでOCamlです。

簡単な式の評価器を証明駆動開発

EvalML1Errにおける評価の全域性の証明でML1*1のすべての式に評価される値が存在することが分かったので、式を評価する関数書いてみたいと思います。また、せっかくCoqで書いたので関数が妥当であるかの証明とOCamlソースコードの出力も行おうと思います。 *…

型推論書いたった

タイトルの通り、OCamlでOCamlのサブセットの型推論を書いたので、その事について纏めておこうと思います。

プログラミング言語の基礎概念の演習問題を解くプログラム

プログラミング言語の基礎概念と言う意味論や型理論の入門に良さげな本が有るんですが、この本は嬉しいことにオンライン演習システムが有るので実際に手を動かしながら内容を理解することができます。