Coqに入門した感想 - 未完成な論を綴るブログ
最近、定理証明支援のCoqを入門している。というのは、以前の職場にいたときの職場でもCoqをやっている先輩がいて、今回の職場でも定理証明支援系を使っている同僚がいて、しかも最近自分はプログラミング言語実装をやっているためか、Coqや依存型について聞かれることがあるので、一念発起して取り組み始めた。 しかし、案の定、何から始めたらいいのかわからず入門に躓いてしまい、かなり難しいと感じた。しかも一番最初に読み始めた本が、Certified Programming with Dependent Typeという初心者向けではない本だったため、事態は混迷を極めていた。 そんな難関を乗り越えて2ヶ月、ようやく基本的な証明をできるまでたどり着いたので、メモ代わりにどう入門すればよいか残しておこうと思う。 1. 関数型のプログラミング言語を学ぶ 自分は関数型プログラミング言語の処理系を設計・実装したことが
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する - エンジニアHub｜Webエンジニアのキャリアを考える！
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する プログラミング言語「Coq」では、プログラムを「証明」して間違いを防ぐことができます。プログラムの正しさを保証できる一歩進んだエンジニアになりましょう！ coqtokyoを主催する今井宜洋さんの解説です。 みなさん、Coqってご存知ですか？ プログラムを証明して間違いを防ぐという優れものです。今回はそのCoqについて、coqtokyoという勉強会を主催している今井宜洋がお届けします。 プログラムをただ作るだけではなく、その正しさを保証できる一歩進んだエンジニアになってみましょう！ Coqって何？ プログラムを「証明する」ってどういうこと？ Coqを使ってみよう Coqのインストール方法 CoqIDE：Coqによる証明開発のフロントエンド Coqで関数プログラミング プログラムの仕様を記述しよう 証明開発モード ゴ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
