現在おしらせはありません
ProofCafeではいくつかの勉強会を定期開催しています。 詳細は個別のページをご覧ください。
Coqを用いたプログラムの証明について勉強する勉強会です。 コーヒーを飲みながら楽しく証明しましょう。
Types and Programming Laungages(通称TAPL)の読書会です。 ScalaやF#などの静的型付け言語の基礎になっている型理論について学びます。
圏論に関する勉強会です。
Haskellに関する勉強会です。
Benjamin C. Pierce氏による同名のテキストの和訳です。関数プ ログラミグやラムダ計算についてCoqによる実例を交えながら丁寧 に説明されています。
Coqの定理検索サービスです。
Coqによる任意精度の計算機です。
数学についてのいくつかのトピックに関する解説です。
型によるOCaml APIの検索です。
CoqのExtraction機能を拡張し、他言語への変換をサポートします。
ターミナルで動作するTwitterクライアントです。一部がCoqにより証明されています。
Msgpackは軽量・高速を特徴とするオブジェクトシリアライザです。 Coqにより変換の正しさが証明されています。
OCamlの対話環境をAndroidに移植したものです。
式の型を表示するコンパイラ拡張です。