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

チェシャ猫の消滅定理

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

LiquidHaskell コトハジメ

このエントリは Haskell Advent Calendar 2016 および Formal Method Advent Calendar 2016 の 23 日目の投稿です。のはずでしたがすでに日付が変わりました。謹んでお詫び申し上げます。 ちなみに 22 日目の担当者はそれぞれ Haskell Advent Calendar 2016 …

NGK2016B で Kubernetes + Alloy について話してきました

先日、毎年恒例のなごや LT 大会 NGK2016B / 名古屋合同懇親会 2016 忘年会 で発表してきました。 机上の Kubernetes - 形式手法で見るコンテナオーケストレーション #NGK2016B from y_taka_23 www.slideshare.net 当日の動画は NGK 2016B LT #2 - YouTube …

Frege のチュートリアル集「Frege Goodness」を翻訳しました

Frege のチュートリアル集を日本語に翻訳しました。原著は Dierk Koenig 氏による Frege Goodness · GitBook です。 www.gitbook.com 対象読者 まえがきでも述べられている通り、Frege の (すなわち Haskell の) 基本的な文法については既知のものとして扱わ…

Frege からメールが送信できるようになりました

ちょっとした Web アプリを作成しようと思うと、メール送信機能がないと困ります。例えば、ログイン機能を持っていれば必然的にパスワードリセットとかも必要になりますからね。 Haskell 風の JVM 言語 Frege でもフレームワーク Chinook を使用して Web ア…

JAWS FESTA 東海道 2016 で形式手法によるネットワーク設計について話してきました

先日行われた JAWS FESTA 東海道 2016 で登壇してきました。 形式手法と AWS のおいしい関係。- モデル検査器 Alloy によるインフラ設計技法 #jawsfesta from y_taka_23 www.slideshare.net テーマは以前 AWS Summit で発表したものと同じですが、前回が 5 …

AWS Summit Tokyo 2016 で形式手法について話してきました

先日行われた AWS Summit Tokyo 2016 で、形式手法のインフラ設計への応用について発表してきました。 形式手法で捗る!インフラ構成の設計と検証 from y_taka_23 www.slideshare.net モデル検査器 Alloy を利用して AWS の設定を検査する、という内容の LT …

NL 名古屋で Frege の評価戦略について話してきました

先日の 歌舞伎座.tech に引き続き、NL名古屋 - connpass で Haskell 風 JVM 言語 Frege について発表してきました。 今回の発表では、Frege の持つ Haskell 的特徴である非正格評価に焦点を当て、正格評価を行うはずの Java 上でなぜ評価を遅延させられるの…

歌舞伎座.tech #9 で Frege について話してきました

先日行われた 歌舞伎座.tech#9「異種プログラミング言語格闘勉強会」 - connpass で Haskell 風 JVM 言語である Frege について発表してきました。 今回の勉強会のテーマは「様々な言語に触れて視野を広げる」ということだったので、細かな言語仕様にはあえ…

すごい JVM 言語 Frege をたのしく学ぼう!

言わずと知れた Haskell の定番教科書『すごい Haskell たのしく学ぼう!』に登場するサンプルコードを、プログラミング言語 Frege に翻訳してみました。 github.com Frege について Frege は、JVM 上で動く純粋関数型プログラミング言語です。 github.com …

Alloy で自動定理証明っぽいやつ

このエントリは Theorem Prover Advent Calendar 2015 - Qiita の 23 日目です。 とは言ってみたものの、内容はいわゆる定理証明器の話ではありません。モデル検査器 Alloy を利用して古典命題論理のシークエント計算をモデル化し、証明図を自動生成させるこ…

NGK2015B で AWS + Alloy について話してきました

先日、毎年恒例のなごや LT 大会 NGK2015B / 名古屋合同懇親会 2015 忘年会 で発表してきました。 AWS は形式手法の夢を見るか? - モデル検査器 Alloy によるインフラ設計 from y_taka_23 www.slideshare.net 当日の動画は [3] NGK2015B(名古屋合同懇親会 …

第十二回渋谷 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…