チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

第十二回渋谷 Java で Featherweight Java の話をしてきました

8 月 1 日に行われた第十二回渋谷 Java で Java の型システムについて LT をしてきました。以下が使用したスライドです。 Hello, Type Systems! - Introduction to Featherweight Java from y_taka_23 ちなみに Featherweight Java を導入した論文はここで読…

稼働中の Docker コンテナ内にファイルを転送するツール Docker Inject を作ってみました

ホスト側から run 中の Docker コンテナ内へ、ディレクトリごとコピーします。 y-taka-23/docker-injectgithub.com 背景 Docker を運用している上で、動いているコンテナの中にファイルを送り込みたくなったことはないでしょうか。ないですか? 残念ながらあ…

Dockerfile をパラメータ化するツール VoicePipe を作ってみました

ひとつの Dockerfile から複数の Docker イメージをビルドすることができます。 y-taka-23/voicepipegithub.com 背景 インフラ環境まわりを Docker 化している場合、しばしば複数の Docker イメージを同時並行的に管理する必要が生じます。例えばミドルウェ…

NGK2014B で SPIN について話してきました

名古屋工業大学で行われた LT 大会 NGK2014B で発表しました。内容はタイトルそのままで、モデル検査ツール SPIN とその記述言語である Promela の特徴を概観する、というものです。 猫でもわかる! モデル検査器 SPIN 入門 from y_taka_23 当日の動画は You…

Coq で Quine

Coq で自己出力プログラム、いわゆる Quine を作成してみました。全体の流れとしては情報処理学会の連載「自分自身を出力するプログラム」の Haskell 版を参考にしてあります。今回のコードは短いので記事の最後に全体を載せてありますが、一応いつものごと…

Coq でクイックソート (3)

Coq でクイックソートの検証、三回目です。今回は最後に残った部分をちょろっとだけ埋めましょう。コードは前回、前々回に追記する形で、https://gist.github.com/4526374 に置いてありますのでよかったらご参照を。 アルゴリズムの定義 仕様の検証その 1 仕…

Coq でクイックソート (2)

Coq でクイックソートの検証、二回目です。コードは前回のものに追記する形で https://gist.github.com/4526374 に置いてあります。 アルゴリズムの定義 仕様の検証その 1 (この記事) 仕様の検証その 2 今回の目標 さて、前回の最後にも触れた通り、前回定義…

Coq でクイックソート (1)

以前の記事「Coq で filter 関数」の最後にちょっと触れた通り、Coq でクイックソートを扱ってみます。ひとつの記事にすると長くなりそうなので、全 3 回に分割してみました。 アルゴリズムの定義 (この記事) 仕様の検証その 1 仕様の検証その 2 ちなみに、…

Coq で位相空間

前々回の記事「Coq でモジュラー束」で「群 G の部分群を述語 G -> Prop で表す」という方針を採用したところ、割と上手くいくということがわかりました。今回は他の題材として、「連結集合の連続写像による像は連結」であることを、同じ方針により証明して…

Coq で filter 関数

リストの要素の内、条件に合致するものだけを抜き出す関数 filter の仕様を Coq で証明してみました。元ネタは『ソフトウェアの基礎』の練習問題。完全なコードは https://gist.github.com/4401408 に置いてあります。 とりあえず定義の確認 List モジュール…

Coq でモジュラー束

この記事は LL/ML Advent Calendar の 23 日目です。「タイトルに "LL" もしくは "ML" を含むこと」という謎ルールに従い、「群の正規部分群の全体がモジュラー束 (Modular Lattices) をなすこと」を Coq により証明してみました。なお、完全なコードは http…