fetburner.hatenablog.com
doi.org
fetburner.hatenablog.com
doi.org
東北大学 / 大学院情報科学研究科
もっと二分探索に証明を付ける
以前二分探索の正当性をCoqで証明しましたが，この証明スクリプトからOCamlのコードを抽出して実際に競プロに用いようとすると，添字の動く範囲が保証されていないので添字エラーを起こすこともしばしばでした． そこで，依存型を活用して添字の動く範囲も保証しようと思います．
400万人が利用するビジネスSNS
水野 雅之
ウォンテッドリー株式会社 / エンジニア
自己紹介
ログインユーザーのみに公開
最近のストーリー
/assets/images/7052304/original/49100b17-5866-4cec-b50b-a37ea73565e9?1638782149){kind=avatar}
ウォンテッドリー株式会社5年間
エンジニア現在
- 現在
東北大学
大学院情報科学研究科
-
- 型推論器の形式的検証
MLのサブセット（λ計算をletと参照で拡張したもので，let多相と単純な値制約をサポートする静的型付き言語）の型安全性と，その型推論器の健全性・完全性の，Coqを用いた形式的検証
大学院情報科学研究科
東北大学
工学部情報知能システム総合学科
三年次編入学
香川高専高松キャンパス
電気情報工学科
高専時代に学んだことは情報系より電気系の方が多かったのですが、高専ロボコンで組み込み開発を行ううちに情報系への興味が出てきたため、情報系の学科に編入学する事にしました
限定公開の職歴・学歴
水野 雅之さん
のプロフィールをすべて閲覧
Wantedlyユーザー もしくは つながりユーザーのみ閲覧できる項目があります
過去の投稿を確認する
共通の知り合いを確認する
水野 雅之さんのプロフィールをすべて見る
スキルと特徴
Ruby
3川崎 禎紀とその他2人が+1
TypeScript
2竹野 創平、塩津 拓真が+1
OCaml
1川崎 禎紀が+1
Coq
1川崎 禎紀が+1
出版と執筆
実績
受賞と資格
言語
- 日本語 - ネイティブレベル