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