fetburner.hatenablog.com
doi.org
fetburner.hatenablog.com
doi.org
東北大学 / 大学院情報科学研究科
もっと二分探索に証明を付ける
以前二分探索の正当性をCoqで証明しましたが，この証明スクリプトからOCamlのコードを抽出して実際に競プロに用いようとすると，添字の動く範囲が保証されていないので添字エラーを起こすこともしばしばでした． そこで，依存型を活用して添字の動く範囲も保証しようと思います．
Business social network with 4M professionals
Mizuno Masayuki
ウォンテッドリー株式会社 / エンジニア
Self Introduction
Available to logged-in users only
Recent stories
/assets/images/7052304/original/49100b17-5866-4cec-b50b-a37ea73565e9?1638782149){kind=avatar}
ウォンテッドリー株式会社5 years
エンジニアPresent
- Present
東北大学
大学院情報科学研究科
-
大学院情報科学研究科
東北大学
工学部情報知能システム総合学科
三年次編入学
香川高専高松キャンパス
電気情報工学科
高専時代に学んだことは情報系より電気系の方が多かったのですが、高専ロボコンで組み込み開発を行ううちに情報系への興味が出てきたため、情報系の学科に編入学する事にしました
Hidden: Education and Experience
View Mizuno Masayuki's
Full Profile
This information is visible only to Wantedly users or the user’s connections
View past posts
View mutual connections
View Mizuno Masayuki's full profile
Skills
Ruby
3Recommended by Yoshinori Kawasaki and 2 more
TypeScript
2Recommended by Sohei Takeno, Takuma Shiotsu
OCaml
1Recommended by Yoshinori Kawasaki
Coq
1Recommended by Yoshinori Kawasaki
Publications
Accomplishments / Portfolio
Awards and Certifications
言語
- Japanese - Native