東北大学 / 大学院情報科学研究科
もっと二分探索に証明を付ける
以前二分探索の正当性をCoqで証明しましたが,この証明スクリプトからOCamlのコードを抽出して実際に競プロに用いようとすると,添字の動く範囲が保証されていないので添字エラーを起こすこともしばしばでした. そこで,依存型を活用して添字の動く範囲も保証しようと思います.
400万人が利用する会社訪問アプリ
ウォンテッドリー株式会社 / エンジニア
ログインユーザーのみに公開
https://www.wantedly.com/companies/wantedly/post_articles/548481 について発表
MLのサブセット(λ計算をletと参照で拡張したもので,let多相と単純な値制約をサポートする静的型付き言語)の型安全性と,その型推論器の健全性・完全性の,Coqを用いた形式的検証
研究 https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19J11926/
三年次編入学
水野 雅之さん
のプロフィールをすべて閲覧
Wantedlyユーザー もしくは つながりユーザーのみ閲覧できる項目があります
過去の投稿を確認する
共通の知り合いを確認する
水野 雅之さんのプロフィールをすべて見る
東北大学 / 大学院情報科学研究科
以前二分探索の正当性をCoqで証明しましたが,この証明スクリプトからOCamlのコードを抽出して実際に競プロに用いようとすると,添字の動く範囲が保証されていないので添字エラーを起こすこともしばしばでした. そこで,依存型を活用して添字の動く範囲も保証しようと思います.