水野 雅之

ウォンテッドリー株式会社 / エンジニア

水野 雅之

ウォンテッドリー株式会社 / エンジニア

東京

水野 雅之

ウォンテッドリー株式会社 / エンジニア

あなたも Wantedly で
プロフィールを作りませんか?

これまでの経歴を、あなたの想いや挑戦とともに表現しよう。

いますぐ作る

つながってこの人をもっと知ろう

自己紹介などの詳しいプロフィールは、つながりをリクエストして承認されると表示できます。

2020年10月
-
現在

エンジニア
現在

2020年10月 -

現在

2020年10月 -

現在

最小共通祖先を求めるアルゴリズムの形式検証

2021年9月

ダイクストラ法の一般化と,その正当性の Coq を用いた検証 - fetburner.core

2021年3月

gRPC Ruby でハマらないための型チェッカー

2021年1月

効率的な正規表現エンジンを Coq で検証する - fetburner.core

2020年12月

ML のサブセットの型推論器を Coq で検証する

2020年12月

2016年4月
-
2020年9月

東北大学

大学院情報科学研究科

2016年4月 - 2020年9月

東北大学

大学院情報科学研究科

2016年4月 - 2020年9月

型推論器の形式的検証

MLのサブセット(λ計算をletと参照で拡張したもので,let多相と単純な値制約をサポートする静的型付き言語)の型安全性と,その型推論器の健全性・完全性の,Coqを用いた形式的検証

2020年6月

フロイドの循環検出アルゴリズムの形式的検証

2020年5月

Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion

2019年12月

もっと二分探索に証明を付ける

2018年5月

大学院情報科学研究科

Formal Verification of the Correspondence between Call-by-Need and Call-by-Name

2018年4月

2019年4月
-
2020年6月

特別研究員DC2

2019年4月 - 2020年6月

研究 https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19J11926/

特別研究員DC2

2019年4月 - 2020年6月

研究 https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19J11926/

2016年3月

東北大学

工学部情報知能システム総合学科

2016年3月

三年次編入学

東北大学

工学部情報知能システム総合学科

2016年3月

三年次編入学

2014年3月

香川高専高松キャンパス

電気情報工学科

2014年3月

香川高専高松キャンパス

電気情報工学科

2014年3月


スキルと特徴

Ruby

Kokoro Higuchiとその他2人が +1
3

OCaml

Yoshinori Kawasakiが +1
1

Coq

Yoshinori Kawasakiが +1
1

Publications

最小共通祖先を求めるアルゴリズムの形式検証

2021年9月

ダイクストラ法の一般化と,その正当性の Coq を用いた検証 - fetburner.core

2021年3月

gRPC Ruby でハマらないための型チェッカー

2021年1月

効率的な正規表現エンジンを Coq で検証する - fetburner.core

2020年12月

ML のサブセットの型推論器を Coq で検証する

2020年12月

さらに表示

Accomplishments/Portfolio

型推論器の形式的検証

2020年6月

Awards and Certifications

修士(情報科学)

2018年3月

学士(工学)

2016年3月


言語

日本語 - ネイティブ