CV
amutake
コード
https://github.com/amutake
技術的興味
分散システム
ネットワークプロトコル
型システム
定理証明
プログラミング言語 (仕事でそこそこ使ったことがある言語)
Erlang
2016.06~2019.03 仕事で
OCaml
2018.11~2019.03 仕事で
Coq
2013.04~2018 研究/仕事で
Haskell
2012.12~2014 アルバイトで
2019.03~ 仕事で
Scala
2014~2015 アルバイトで
JavaScript
2015 アルバイトで
Ruby
2015.04 インターンで
Go
2020.01~ 仕事で
その他少しなら触ったことがある言語 (順不同)
C, C++, Elixir, Python, Rust, Dart, TypeScript, Haxe, Java, Scheme, Emacs Lisp, Idris ...
作ったもの (まじめに作ったもの)
sluicegate
OSS ではない
メディアストリームを複数のノードに中継するミドルウェア
https://niconare.nicovideo.jp/watch/kn3115
Actario
アクターシステムをCoqで検証するフレームワーク
https://github.com/amutake/actario
expeditor
なにか失敗する可能性のあるタスクを非同期に実行するRubyライブラリ (主にマイクロサービス呼び出しに使われることが多い)
https://github.com/cookpad/expeditor
発表・本・論文・ポスターなど (上から新しい順)
進捗大陸07
ProveEverywhere v2の話
https://shinchoku-tairiku.github.io/web/books/tairiku07/
進捗大陸06
SATySFiで技術同人誌を書く話
https://shinchoku-tairiku.github.io/web/books/tairiku06/
進捗大陸05
CRDTsの話
https://shinchoku-tairiku.github.io/web/books/tairiku05/
進捗大陸04
技術書典05に出した合同誌
RustでQUICを実装する話を書いた
https://shinchoku-tairiku.github.io/web/#shinchoku_tairiku_04
Erlang 事例紹介: メディアストリーム中継システム
Erlang & Elixir Fest. 2018 での発表
sluicegate のモチベーション、概要、工夫したところの話
https://speakerdeck.com/amutake/erlang-shi-li-shao-jie-medeiasutorimuzhong-ji-sisutemu
https://niconare.nicovideo.jp/watch/kn3115 (404)
進捗大陸03
技術書典04に出した合同誌
Erlangのバイトコードにコンパイルされる静的型付き言語Alpacaという言語についての紹介を書いた
https://shinchoku-tairiku.github.io/web/#shinchoku_tairiku_03
生放送ストリーム中継システムのCoqによる形式化と検証
PPL2018 に投稿したポスター
sluicegate のバッファ部分 (のサブセット) を Coq で検証した話
https://jssst-ppl.org/workshop/2018/program.html
進捗大陸02
技術書典03に出した合同誌
自分は Verdi という Coq のフレームワークで証明付き分散システムを作る話を書いた
https://shinchoku-tairiku.github.io/web/#shinchoku_tairiku_02
進捗島
技術季報 Vol.2 に寄稿
分散システムを形式手法を使って検証する話
https://techbookfest.org/journal/2
進捗大陸01
技術書典02に出した合同誌
自分は Erlang に型を付けたいという話 (成功型付けとMLsub) を書いた
https://shinchoku-tairiku.github.io/web/#shinchoku_tairiku_01
Actario: 定理証明支援系Coqによるアクターシステムの検証
PPL2016 に投稿したポスター
Actarioを使うとこうやってアクターシステムを検証できますよ、という話
http://www.psg.cs.titech.ac.jp/posts/2016-03-07-PPL2016.html
w8lt
M2のときに近くの研究室 (西8号館) でやっていたLT会
https://speakerdeck.com/amutake
外に出したくないもの以外はここに
https://w8lt.connpass.com/
Actario: A Framework for Reasoning About Actor Systems
AGERE2015 というアクターモデル関連のワークショップに投稿した論文 (査読付き)
Actarioに関する英語の発表
https://2015.splashcon.org/event/agere2015-actario-a-framework-for-reasoning-about-actor-systems
Actario: Coqによるアクターモデルの形式化とErlangへのコード抽出
PPL2015 に投稿したポスター
CoqからErlangへの変換器を作ったよ、という話
http://www.psg.cs.titech.ac.jp/posts/2015-03-04-PPL2015.html
Aπ計算のCoqによる形式化
JSSST2014 に投稿した論文
Aπ計算というπ計算に型を付けてアクターモデルとしての振る舞いを強制した体系があるけれども、それを Coq で形式化したよ、という話
https://jssst2014.wordpress.com/program/#ppl7
その他 (技術関係ないもの)
高校時代および灯雪会というサークルで行灯 (ねぶたみたいな人形型の灯籠) を作っている
https://satsukita-andon.com
http://tousetsukai.org
アイコンのてるてる坊主も行灯
#キャリア