ProofCafe

ProofCafeは名古屋を中心に活動する定理証明器・関数型言語のコミュニティです。

このエントリーをはてなブックマークに追加

おしらせ

9/12(土)にProofSummit 2015を計画しています。

開催勉強会

ProofCafeではいくつかの勉強会を定期開催しています。 詳細は個別のページをご覧ください。

ProofCafe

Coqを用いたプログラムの証明について勉強する勉強会です。 コーヒーを飲みながら楽しく証明しましょう。

TAPL-nagoya

Types and Programming Laungages(通称TAPL)の読書会です。 ScalaやF#などの静的型付け言語の基礎になっている型理論について学びます。

休日カフェタイム, KCTNagoya

圏論に関する勉強会です。

どえりゃあ Haskell

Haskellに関する勉強会です。

サービス

Software Foundations(和訳)

Benjamin C. Pierce氏による同名のテキストの和訳です。関数プ ログラミグやラムダ計算についてCoqによる実例を交えながら丁寧 に説明されています。

Cochin

Coqの定理検索サービスです。

CalCoq

Coqによる任意精度の計算機です。

数理大好き

数学についてのいくつかのトピックに関する解説です。

OCaml API Search

型によるOCaml APIの検索です。

成果物

Coq Extraction機能の拡張

CoqのExtraction機能を拡張し、他言語への変換をサポートします。

OCamltter

ターミナルで動作するTwitterクライアントです。一部がCoqにより証明されています。

Msgpack for OCaml

Msgpackは軽量・高速を特徴とするオブジェクトシリアライザです。 Coqにより変換の正しさが証明されています。

OCaml Toplevel on Android

OCamlの対話環境をAndroidに移植したものです。

SML# + annot

式の型を表示するコンパイラ拡張です。

過去のイベント