Discover companies you will love
ウォンテッドリー株式会社 / エンジニア
Available to logged-in users only
/assets/images/7052304/original/49100b17-5866-4cec-b50b-a37ea73565e9?1638782149){kind=avatar}
https://www.wantedly.com/companies/wantedly/post_articles/548481 について発表
MLのサブセット（λ計算をletと参照で拡張したもので，let多相と単純な値制約をサポートする静的型付き言語）の型安全性と，その型推論器の健全性・完全性の，Coqを用いた形式的検証
研究 https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19J11926/
三年次編入学
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
Ruby
Recommended by Yoshinori Kawasaki and 2 more
+4 more
+18 more
+1 more
+1 more
東北大学 / 大学院情報科学研究科
今となっては少々昔のことですが，AtCoder Beginner Contest 167のD問題で数列の循環検出が必要になった事がありました（問題の制約的にはダブリングでも解けますが）． 数列の循環検出はナイーブにに実装すると，循環している部分に至るまでの長さを，循環の長さをとするとのメモリが必要になってしまいますが，これをで計算するアルゴリズムとして，フロイドの循環検出法が知られています． 中々巧妙なアルゴリズムなもので，これを実装して本当に循環検出ができているのか少々不安に思うところもありますし，この際Coqで正当性を保証してやりましょう．
wantedly.com
wantedly.com
fetburner.hatenablog.com
doi.org
fetburner.hatenablog.com
doi.org
