著者
アフェルト レナルド
雑誌
情報処理
巻号頁・発行日
vol.55, no.5, pp.482-491, 2014-04-15

近年,定理証明支援系による成功が続いている:数学の証明の形式化,コンパイラやオペレーティングシステムの検証,などである.近年,定理証明支援系が数学とセキュアなコンピュータシステムの構築に欠かせないツールになってきており,本稿では,定理証明支援系による実例を紹介し,代表的な定理証明支援系Coqの基本的な使い方を説明する.

言及状況

Facebook (1 users, 1 posts)

アフェルト レナルド:定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-,情報処理,Vol.55,No.5,pp.482-491(2014).

Facebook における性別

はてなブックマーク (1 users, 2 posts)

アフェルト レナルド:定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-,情報処理,Vol.55,No.5,pp.482-491(2014).
アフェルト レナルド:定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-,情報処理,Vol.55,No.5,pp.482-491(2014).

Twitter (5 users, 5 posts, 0 favorites)

@sanjutsu_yu このへんにCoqでの同値関係の理屈書いてて、まあこれ自体は納得できるのですが実装がわからない https://t.co/EbmkFiz5Zb https://t.co/Mm91GteY7H
定理証明支援系 https://t.co/VFZc7js6hV
アフェルト レナルド:定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-,情報処理,Vol.55,No.5,pp.482-491(2014). / “情報学広場:情報処理学会電子図書館” http://t.co/lrjb5NJsvD

収集済み URL リスト