チェシャ猫の消滅定理

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

詳解! Elm における Fuzzing

先日行われた We Are JavaScripters! @23rd で、Elm のテストフレームワーク elm-test に搭載されている Fuzzing 機能について発表してきました。 Fuzzing を利用するとテストデータを自動で生成することができるため、例えば「encode と decode を行うと元…

July Tech Festa 2018 で分散システムの検証について話してきました / #JTF2018

先日行われた July Tech Festa 2018 で、モデル検査を使った分散アルゴリズムの検証について発表してきました。 前半はオートマトンによるシステムの記述と検査の基礎について、後半は三種類のツール SPIN、TLA+、P による記述方法の紹介、といった内容です…

We Are JavaScripters! @19th で Haskell 製フレームワーク Miso について話してきました

先日行われた We Are JavaScripters! @19th で Haskell によるフロントエンド開発について発表してきました。 Elm の代わりにフレームワーク Miso を使うことで、クライアントサイドとサーバサイドの両方を Haskell で実装することができる、という内容です…

JAWS DAYS 2018 で形式手法による IAM の検証について話してきました

だいぶ日が空いてしまって今更ですが、先日行われた JAWS DAYS 2018 で登壇してきました*1。モデル検査器 Alloy を使って AWS の IAM を検証してみるという内容です。 形式手法 × AWS というテーマではこれまでにもいくつかのイベントで発表していますが、題…

Kubernetes Meetup Tokyo #10 で Pod の Preemption について話してきました

だいぶ日が空いてしまって今更ですが、先日行われた Kubernetes Meetup Tokyo #10 で、v1.9 から導入された新機能 Preemption について発表してきました。 Preemption は、Kubernetes クラスタのリソースが不足した際に、優先度が低い Pod を追い出して優先…

猫でもわかる rkt + Kubernetes

このエントリは Kubernetes Advent Calendar 2017 の 23 日目の記事です。ちなみに昨日は takezaki さんの「GCBを利用したContinuous Delivery環境」でした。 LT で使用したスライド 先日、市ヶ谷Geek★Night #16 の 10 分 LT 枠で、CoreOS 社によるコンテナ…

NGK2017B で Liquid Haskell について話してきました

先日、毎年恒例のなごや LT 大会 NGK2017B / 名古屋合同懇親会 2017 忘年会 で発表してきました。 Liquid Haskell で普通の型システムの上を行け #NGK2017B from y_taka_23 www.slideshare.net 当日の動画は NGK2017B 第2部 - YouTube から見ることができ…

現在時刻をモックする Haskell ライブラリ time-machine を作ってみました

主としてテスト時のために、現在時刻を操作する Haskell ライブラリを作成しました。Hackage にも登録済みです。 github.com 試しに次のコードを実行してみましょう。getCurrentTime しているはずなのに、返ってくる値が 1985 年 10 月 26 日になっているは…

技術書典 3 で新刊落としました

先日、秋葉原で開催された技術系同人誌のオンリーイベント 技術書典 3 にサークル参加しました。 本当は新刊として Scala 用の静的解析ツール Stainless の入門書を頒布する予定で、サークルカットも完全にその線で準備していたのですが、残念ながら諸事情に…

Serverless Meetup Tokyo #6 で Kubernetes について話してきました

先日行われた Serverless Meetup Tokyo #6 で、Kubernetes 上で動作する Serverless フレームワーク Fission について発表してきました。 Fission で 始める Containerless Kubernetes #serverlesstokyo from y_taka_23 www.slideshare.net 先週も 似たよう…

Kubernetes Meetup Tokyo #7 で Serverless について話してきました

先日行われた Kubernetes Meetup Tokyo #7 で、Kubernetes 上で動作する Serverless フレームワークについて発表してきました。 Kubernetes でも Serverless したい! #k8sjp from y_taka_23 www.slideshare.net Serverless on Kubernetes を謳うツールはい…

Haskell ライブラリにスターを送るツール thank-you-stars を作ってみました

Haskell の GitHub レポジトリを眺めてみると、有名ライブラリであってもスター数が意外と少ないことがあります。かの Yesod ですら本記事執筆時点で 1,794 個であり、Rails の 36,933 個や Django の 28,165 個と比較すると文字通り桁違いです。 スター数は…

JJUG CCC 2017 Spring で Haskell on JVM について話してきました

先日行われた JJUG CCC 2017 Spring で、JVM 上で動作する Haskell について発表してきました。 思ったほど怖くない! Haskell on JVM 超入門 #jjug_ccc #ccc_l8 from y_taka_23 www.slideshare.net メインになるコンテンツはふたつの JVM 言語、Frege と Et…

超技術書典で同人誌『入門 LiquidHaskell』を頒布できませんでした

先日、ニコニコ超会議内で行われた「超技術書典」にて、LiquidHaskell の同人誌でサークル参加してきました。 lh101.dodgsonlabs.com 技術書典 2 ではそこそこの部数が出た ので Haskell 同人誌の需要はゼロではないと踏んでいたのですが、びっくりするぐら…

技術書典 2 で同人誌『入門 LiquidHaskell』を頒布しました

先日、秋葉原で行われた技術書のオンリーイベント「技術書典 2」にて、LiquidHaskell の同人誌を頒布してきました。 lh101.dodgsonlabs.com LiquidHaskell は、SMT ソルバをバックエンドとして利用することで、Haskell の持つ型の表現力をより強化する仕組み…

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…