水野 雅之

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

水野 雅之

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

水野 雅之

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

Why not create your own Wantedly profile?

Showcase yourself and your experiences to bring your professional story to life.

Join

Connect to learn more

You'll be able to see their introduction and other information once they have accepted your connection request.

Oct 2020
-
Present

エンジニア
Present

Oct 2020 -

Present

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

Mar 2021

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

Jan 2021

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

Dec 2020

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

Dec 2020

Apr 2016
-
Sept 2020

東北大学

大学院情報科学研究科

Apr 2016 - Sept 2020

型推論器の形式的検証

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

June 2020

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

May 2020

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

Dec 2019

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

May 2018

大学院情報科学研究科

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

Apr 2018

Apr 2019
-
June 2020

特別研究員DC2

Apr 2019 - June 2020

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

Mar 2016

東北大学

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

Mar 2016

三年次編入学

Mar 2014

香川高専高松キャンパス

電気情報工学科

Mar 2014


Skills and qualities

Ruby

Recommended by Kokoro Higuchi and 2 more
3

OCaml

Recommended by Yoshinori Kawasaki
1

Coq

Recommended by Yoshinori Kawasaki
1

Publications

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

Mar 2021

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

Jan 2021

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

Dec 2020

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

Dec 2020

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

May 2020

Show more

Accomplishments/Portfolio

型推論器の形式的検証

June 2020

Awards and Certifications

修士(情報科学)

Mar 2018

学士(工学)

Mar 2016


Languages

Japanese - Native