今井宜洋

証明エンジニア
ソフトウェアエンジニア

仕事

(2019.09 ~ now) 株式会社proof ninja 代表取締役社長
(2017.04 ~ 2019.08) 株式会社ドワンゴのソフトウェアエンジニア
(2012 ~ 今) TopSEの講師
(2016, 2017, 2019) 名古屋大学客員准教授
(2007.04 ~ 2017.02) 有限会社ITプランニングのソフトウェアエンジニア

連絡先

E-mail: yoshihiro503 at proofcafe.org
Twitter: @yoshihiro503

ソフトウェア

著書

発表、講演

2007 「Coq、定理証明という選択肢」 Lightweight Language 魂
2008 「超未来言語 Gallina」 Lightweight Language Future
2009 「OCamlでらくらく関数型プログラミング」オープンソースカンファレンスNagoya
2010 「システム開発実務への証明支援器Coqの適用」第12回プログラミングおよびプログラミング言語ワークショップ
2010 「はじめてのCoq」 Coq庵
2011 「形式手法の現在と実開発への適用可能性」 QCon Tokyo 2011
2011 Coq チュートリアル - Top SE
2011 特殊研究1 at 京都大学情報科学研究科
2011 高信頼ソフトウェア開発における数学 - 名古屋大学キャリアアップセミナー
2012 Coq 特別講義 - Top SE
2012 The Algorithm M'_annot for Coq Extractionto Statically Typed Languages without Type Inference - ML名古屋
2012 Scalaで学ぶSEのための実践的関数型言語入門 - Top SE
2012 「関数型プログラミング言語と証明支援器を使った金融情報システムの開発について」 - 第3回形式手法の産業応用ワークショップ
2014 「なぜCoqは重要か」スタートSsreflect
2014 「Coqを使ったデジタルデータ放送におけるストリームデータ処理の形式化と検証」高信頼な理論と実装のための定理証明および定理証明器
2014 A Coq Application in a Broadcast System - Proof Summit 2014
2016 Base 常用漢字e ncoding with geNeraLized Base-N encoding - NL名古屋
2017 初めて学ぶCoq - Proof Summit 2017
2017 転職してみた - 名古屋合同懇親会2017
2018 生放送ストリーム中継システムのCoqによる形式化と検証 - 第20回プログラミングおよびプログラミング言語ワークショップ
2018 ニコニコをCoqで証明してみた - Proof Summit 2018

学会委員等

プログラミングおよびプログラミング言語ワークショップ 2011 (プログラミング委員)
第83回情報処理学会

参加している技術勉強会