おしらせ
現在おしらせはありません
開催勉強会
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
式の型を表示するコンパイラ拡張です。
過去のイベント
- ProofSummit 2019(2019/09/29)
- ProofSummit 2018(2018/09/02)
- ProofSummit 2017(2017/07/23)
- ProofSummit 2016(2016/09/25)
- ProofSummit 2015(2015/09/12)
- ProofSummit 2014(2014/09/06)
- StartSsreflect(2014/04/26)
- ProofSummit 2013(2013/08/24)
- Proof Summit 2012(2012/09/02)
- ML名古屋(2012/05/26)
- スタートSML#(2012/03/25)
- ProofSummit(2011/09/25)
- Coq Party(2010/11/27)
- Coq庵(2010/08/29)
- 名古屋Hackathon(ラムダ村)(2010/10/09)