今井宜洋

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

仕事

(2022.11 ~ now) 合同会社DMM.com 形式証明エンジニア
(2022.09 ~ now) 国立産業技術総合研究所超分散トラスト研究チーム
(2019.09 ~ now) 株式会社proof ninja 設立、代表取締役 CEO 就任
(2020 ~ now) 名古屋大学客員教授
(2017.04 ~ 2019.08) 株式会社ドワンゴのソフトウェアエンジニア
(2012 ~ 今) TopSEの講師
(2016, 2017, 2019) 名古屋大学客員准教授
(2007.04 ~ 2017.02) 有限会社ITプランニングのソフトウェアエンジニア

連絡先

E-mail: y.imai at proof-ninja dot co.jp, y.imai at aist.go.jp, imai-yoshihiro at dmm.com
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
2020 関数型で世界一安全なお金の取引 - 名古屋合同懇親会2020新年会
2021 関数型言語OCamlと形式手法で証明されたブロックチェーンプログラミング - 第一回関数型プログラミング（仮）の会
2023 関数型言語使いのための形式証明入門 - 第四回関数型プログラミング（仮）の会
2023 数学の証明でバグをなくす！？形式手法Coqの紹介 - 株式会社DM2C Studio DMM.com Web3事業部勉強会
2024 関数型でブロックチェーンプログラミング - 第五回関数型プログラミング（仮）の会

学会委員等

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

参加している技術勉強会