だいぶ日が空いてしまって今更ですが、先日行われた JAWS DAYS 2018 で登壇してきました*1。モデル検査器 Alloy を使って AWS の IAM を検証してみるという内容です。 形式手法 × AWS というテーマではこれまでにもいくつかのイベントで発表していますが、題…
だいぶ日が空いてしまって今更ですが、先日行われた Kubernetes Meetup Tokyo #10 で、v1.8*1 から導入された新機能 Preemption について発表してきました。 Preemption は、Kubernetes クラスタのリソースが不足した際に、優先度が低い Pod を追い出して優…
このエントリは Kubernetes Advent Calendar 2017 の 23 日目の記事です。ちなみに昨日は takezaki さんの「GCBを利用したContinuous Delivery環境」でした。 LT で使用したスライド 先日、市ヶ谷Geek★Night #16 の 10 分 LT 枠で、CoreOS 社によるコンテナ…
先日、毎年恒例のなごや LT 大会 NGK2017B / 名古屋合同懇親会 2017 忘年会 で発表してきました。 Liquid Haskell で普通の型システムの上を行け #NGK2017B from y_taka_23 www.slideshare.net 当日の動画は NGK2017B 第2部 - YouTube から見ることができ…
主としてテスト時のために、現在時刻を操作する Haskell ライブラリを作成しました。Hackage にも登録済みです。 github.com 試しに次のコードを実行してみましょう。getCurrentTime しているはずなのに、返ってくる値が 1985 年 10 月 26 日になっているは…
先日、秋葉原で開催された技術系同人誌のオンリーイベント 技術書典 3 にサークル参加しました。 本当は新刊として Scala 用の静的解析ツール Stainless の入門書を頒布する予定で、サークルカットも完全にその線で準備していたのですが、残念ながら諸事情に…
先日行われた Serverless Meetup Tokyo #6 で、Kubernetes 上で動作する Serverless フレームワーク Fission について発表してきました。 Fission で 始める Containerless Kubernetes #serverlesstokyo from y_taka_23 www.slideshare.net 先週も 似たよう…
先日行われた Kubernetes Meetup Tokyo #7 で、Kubernetes 上で動作する Serverless フレームワークについて発表してきました。 Kubernetes でも Serverless したい！ #k8sjp from y_taka_23 www.slideshare.net Serverless on Kubernetes を謳うツールはい…
Haskell の GitHub レポジトリを眺めてみると、有名ライブラリであってもスター数が意外と少ないことがあります。かの Yesod ですら本記事執筆時点で 1,794 個であり、Rails の 36,933 個や Django の 28,165 個と比較すると文字通り桁違いです。 スター数は…
先日行われた JJUG CCC 2017 Spring で、JVM 上で動作する Haskell について発表してきました。 思ったほど怖くない！ Haskell on JVM 超入門 #jjug_ccc #ccc_l8 from y_taka_23 www.slideshare.net メインになるコンテンツはふたつの JVM 言語、Frege と Et…
先日、ニコニコ超会議内で行われた「超技術書典」にて、LiquidHaskell の同人誌でサークル参加してきました。 lh101.dodgsonlabs.com 技術書典 2 ではそこそこの部数が出た ので Haskell 同人誌の需要はゼロではないと踏んでいたのですが、びっくりするぐら…
先日、秋葉原で行われた技術書のオンリーイベント「技術書典 2」にて、LiquidHaskell の同人誌を頒布してきました。 lh101.dodgsonlabs.com LiquidHaskell は、SMT ソルバをバックエンドとして利用することで、Haskell の持つ型の表現力をより強化する仕組み…
このエントリは Haskell Advent Calendar 2016 および Formal Method Advent Calendar 2016 の 23 日目の投稿です。のはずでしたがすでに日付が変わりました。謹んでお詫び申し上げます。 ちなみに 22 日目の担当者はそれぞれ Haskell Advent Calendar 2016 …
先日、毎年恒例のなごや LT 大会 NGK2016B / 名古屋合同懇親会 2016 忘年会 で発表してきました。 机上の Kubernetes - 形式手法で見るコンテナオーケストレーション #NGK2016B from y_taka_23 www.slideshare.net 当日の動画は NGK 2016B LT #2 - YouTube …
Frege のチュートリアル集を日本語に翻訳しました。原著は Dierk Koenig 氏による Frege Goodness · GitBook です。 www.gitbook.com 対象読者 まえがきでも述べられている通り、Frege の (すなわち Haskell の) 基本的な文法については既知のものとして扱わ…
ちょっとした Web アプリを作成しようと思うと、メール送信機能がないと困ります。例えば、ログイン機能を持っていれば必然的にパスワードリセットとかも必要になりますからね。 Haskell 風の JVM 言語 Frege でもフレームワーク Chinook を使用して Web ア…
先日行われた JAWS FESTA 東海道 2016 で登壇してきました。 形式手法と AWS のおいしい関係。- モデル検査器 Alloy によるインフラ設計技法 #jawsfesta from y_taka_23 www.slideshare.net テーマは以前 AWS Summit で発表したものと同じですが、前回が 5 …
先日行われた AWS Summit Tokyo 2016 で、形式手法のインフラ設計への応用について発表してきました。 形式手法で捗る！インフラ構成の設計と検証 from y_taka_23 www.slideshare.net モデル検査器 Alloy を利用して AWS の設定を検査する、という内容の LT …
先日の 歌舞伎座.tech に引き続き、NL名古屋 - connpass で Haskell 風 JVM 言語 Frege について発表してきました。 今回の発表では、Frege の持つ Haskell 的特徴である非正格評価に焦点を当て、正格評価を行うはずの Java 上でなぜ評価を遅延させられるの…
先日行われた 歌舞伎座.tech#9「異種プログラミング言語格闘勉強会」 - connpass で Haskell 風 JVM 言語である Frege について発表してきました。 今回の勉強会のテーマは「様々な言語に触れて視野を広げる」ということだったので、細かな言語仕様にはあえ…
言わずと知れた Haskell の定番教科書『すごい Haskell たのしく学ぼう！』に登場するサンプルコードを、プログラミング言語 Frege に翻訳してみました。 github.com Frege について Frege は、JVM 上で動く純粋関数型プログラミング言語です。 github.com …
このエントリは Theorem Prover Advent Calendar 2015 - Qiita の 23 日目です。 とは言ってみたものの、内容はいわゆる定理証明器の話ではありません。モデル検査器 Alloy を利用して古典命題論理のシークエント計算をモデル化し、証明図を自動生成させるこ…
先日、毎年恒例のなごや LT 大会 NGK2015B / 名古屋合同懇親会 2015 忘年会 で発表してきました。 AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計 from y_taka_23 www.slideshare.net 当日の動画は [3] NGK2015B（名古屋合同懇親会 …
8 月 1 日に行われた第十二回渋谷 Java で Java の型システムについて LT をしてきました。以下が使用したスライドです。 Hello, Type Systems! - Introduction to Featherweight Java from y_taka_23 ちなみに Featherweight Java を導入した論文はここで読…
ホスト側から run 中の Docker コンテナ内へ、ディレクトリごとコピーします。 y-taka-23/docker-injectgithub.com 背景 Docker を運用している上で、動いているコンテナの中にファイルを送り込みたくなったことはないでしょうか。ないですか？ 残念ながらあ…
ひとつの Dockerfile から複数の Docker イメージをビルドすることができます。 y-taka-23/voicepipegithub.com 背景 インフラ環境まわりを Docker 化している場合、しばしば複数の Docker イメージを同時並行的に管理する必要が生じます。例えばミドルウェ…
名古屋工業大学で行われた LT 大会 NGK2014B で発表しました。内容はタイトルそのままで、モデル検査ツール SPIN とその記述言語である Promela の特徴を概観する、というものです。 猫でもわかる！ モデル検査器 SPIN 入門 from y_taka_23 当日の動画は You…
Coq で自己出力プログラム、いわゆる Quine を作成してみました。全体の流れとしては情報処理学会の連載「自分自身を出力するプログラム」の Haskell 版を参考にしてあります。今回のコードは短いので記事の最後に全体を載せてありますが、一応いつものごと…
Coq でクイックソートの検証、三回目です。今回は最後に残った部分をちょろっとだけ埋めましょう。コードは前回、前々回に追記する形で、https://gist.github.com/4526374 に置いてありますのでよかったらご参照を。 アルゴリズムの定義 仕様の検証その 1 仕…
Coq でクイックソートの検証、二回目です。コードは前回のものに追記する形で https://gist.github.com/4526374 に置いてあります。 アルゴリズムの定義 仕様の検証その 1 (この記事) 仕様の検証その 2 今回の目標 さて、前回の最後にも触れた通り、前回定義…
