この定理証明支援系ツールは、関数型プログラミング言語を基礎としていることが多い。このため、現在の関数型プログラミング言語の流行に乗じて、にわかに注目を集めるようになってきた。(http://proofcafe.org/wiki/)が有名である。Forum(http://groups.google.com/group/fm-forum)が精力的に活動している。2010年には名古屋にて、定理証明支援系ツールのイベント「Coq庵」が開催された(http://coq.g.hatena.ne.jp/keyword/Coq%E5%BA%B5)。国際会議、および併設ワークショップが9月18日から24日にかけて、東京で行われた(http://www.icfpconference.org/icfp2011/)(http://www.icfpconference.org/affiliated.html)。ProofSummit2011である。参加者は総勢約50名という大人数で、会場はほぼ満員の盛況であった。全体的な流れとして、まず午前中に定理証明支援系ツールCoq,Agdaのチュートリアルが行われた。Coqを使用しての簡単な証明のテクニックの解説が行われた。@ikegami__氏によるAgda入門では、Agdaでのプログラミングの基礎から最新機能紹介まで幅広い解説が行われた。参加者からの質問も活発であった。MsgPackのモジュールの証明を行った事例が紹介された。今後のパフォーマンス向上への挑戦が楽しみである。COQ2」という題で、C言語のコードをCoqで証明する技法についての解説が行われた。C言語のような手続き型言語では破壊的代入が頻繁に行われるため、関数型言語のように簡単には証明が行えない。Logicという公理系を使用し、Coqの中にC言語の簡易インタプリタを構築することで、証明を行う方法が紹介された。Logicを使った証明は、ここ数年の間に研究が盛り上がってきた分野である。応用トピックセッションの最後は、@kikx氏による「ssreflect」の解説である。reflection"という、証明スタイルを実現するCoqの拡張ライブラリである。ンテナンスしやすくなる可能性がある。3つのセッションのあとは、8人の方によるライトニングトークが行われた。@masahiro_sakai氏による自動定理証明技術の紹介、@snisimu氏による、回路設計にAgdaを利用する話題等、一人5分では終わらない、濃い解説が印象的だった。次の活動が始まっている。Forumに参加していただきたい。毎週火曜日に前週のまとめコンテンツをお送りいたします。(日本語版は不定期リリース)25万人のシニアな開発者コミュニティーにぜひご参加ください。サンプルを見るあなたのメールアドレスはこちら国を選んでください。プライバシーポリシーに従って私の個人情報を扱うことに同意します。毎週火曜日に前週のまとめコンテンツをお送りいたします。(日本語版は不定期リリース)25万人のシニアな開発者コミュニティーにぜひご参加ください。サンプルを見る様々なイノベーターとアーリーアダプターがお送りするテクノロジーの概要を見る。自分がまだ知らないことに気づいていないと知るあなたが興味のあるトピックスをいつでも最新な情報に。あなたのメールアドレスはこちら国を選んでください。プライバシーポリシーに従って私の個人情報を扱うことに同意します。Inc.プライバシーBT。