iitaka1142 (@iitaka1142)


参加する勉強会

9/15 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Software Foundations VOLUME 2: PROGRAMMING LANGUAGE FOUNDATIONS STLC からです。 TAPLと内容が重なるので、TAPLを持っている方は第9章を読んでおくとよいでしょう。 https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html 前回の復習から始めます。 可能ならば Coq 8.7 をインストールしたうえで、以下よりサンプルコードを入手しておいてください。 https://softwarefoundations.cis.upenn.edu/plf-current/index.html インストール方法などについての質問も常に歓迎です。 以上


過去の勉強会

8/18 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Software Foundations VOLUME 2: PROGRAMMING LANGUAGE FOUNDATIONS STLC からです。 TAPLと内容が重なるので、TAPLを持っている方は第9章を読んでおくとよいでしょう。 https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html 前回の復習から始めます。 可能ならば Coq 8.7 をインストールしたうえで、以下よりサンプルコードを入手しておいてください。 https://softwarefoundations.cis.upenn.edu/plf-current/index.html インストール方法などについての質問も常に歓迎です。 以上

7/21 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Software Foundations VOLUME 2: PROGRAMMING LANGUAGE FOUNDATIONS Type System の Progress からです。 TAPLと内容が重なるので、TAPLを持っている方は第8章を読んでおくとよいでしょう。 https://softwarefoundations.cis.upenn.edu/plf-current/Types.html 前回の復習から始めます。 可能ならば Coq 8.7 をインストールしたうえで、以下よりサンプルコードを入手しておいてください。 https://softwarefoundations.cis.upenn.edu/plf-current/index.html インストール方法などについての質問も常に歓迎です。 以上

6/16 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
(2) 会場の教室に変更はありません。 (3) 次回は、The Software Foundations VOLUME 2: PROGRAMMING LANGUAGE FOUNDATIONS Type System の最初(Typed Arithmetic Expressions)からです。 TAPLと内容が重なるので、TAPLを持っている方は第8章を読んでおくとよいでしょう。 https://softwarefoundations.cis.upenn.edu/plf-current/Types.html 前回の復習から始めます。 可能ならば Coq 8.7 をインストールしたうえで、以下よりサンプルコードを入手しておいてください。 https://softwarefoundations.cis.upenn.edu/plf-current/index.html インストール方法などについての質問も常に歓迎です。 以上 (1) 5月のProofCafeは、OSC名古屋参加のためお休みです。 https://www.ospn.jp/osc2018-nagoya/

4/21 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Software Foundations VOLUME 2: PROGRAMMING LANGUAGE FOUNDATIONS SMALL-STEP OPERATIONAL SEMANTICS の Multi-Step Reduction からです。 https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html 前回の復習から始めます。 可能ならば Coq 8.7 をインストールしたうえで、以下よりサンプルコードを入手しておいてください。 https://softwarefoundations.cis.upenn.edu/plf-current/index.html インストール方法などについての質問も常に歓迎です。 以上

3/17 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Software Foundations VOLUME 2: PROGRAMMING LANGUAGE FOUNDATIONS SMALL-STEP OPERATIONAL SEMANTICS の Strong Progress and Normal Forms からです。 https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html 前回の復習から始めます。 可能ならば Coq 8.7 をインストールしたうえで、以下よりサンプルコードを入手しておいてください。 https://softwarefoundations.cis.upenn.edu/plf-current/index.html インストール方法などについての質問も常に歓迎です。 以上

2/17 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Software Foundations VOLUME 2: PROGRAMMING LANGUAGE FOUNDATIONS SMALL-STEP OPERATIONAL SEMANTICS の Relations からです。 https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html#lab134 前回(初回)の復習から始めます。 可能ならば Coq 8.7 をインストールしたうえで、以下よりサンプルコードを入手しておいてください。 https://softwarefoundations.cis.upenn.edu/plf-current/index.html インストール方法などについての質問も常に歓迎です。 以上

1/20 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
今回(72回)から、Software Foundations から、型付ラムダの章と、Hoare論理の章を読んでいく予定です。 その他の今後予定されるテーマについては、以下を参照してください。 これを取り上げて欲しい、という意見は常に歓迎しています。 https://sites.google.com/site/suharahiromichi/themas 以上

12/30 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
"A Gentle Introduction to Type Classes and Relations in Coq" の第4回目です。 上記を補足するCoqの入門的な資料も用意しますので、安心してください。 また、次に読む文書を選びたいと思います。 以上

11/25 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
"A Gentle Introduction to Type Classes and Relations in Coq" の第3回目です。 予習には、以下を参考に、サンプルコードを読んでおいてください。 準備していなくても、当日、インストールから説明します。 https://github.com/suharahiromichi/doc/blob/master/coq_gitcrc.md また、上記を補足するCoqの入門的な資料も用意しますので、安心してください。 以上

10/21 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
"A Gentle Introduction to Type Classes and Relations in Coq" の第3回目です。 予習には、以下を参考に、サンプルコードを読んでおいてください。 準備していなくても、当日、インストールから説明します。 https://github.com/suharahiromichi/doc/blob/master/coq_gitcrc.md また、上記を補足するCoqの入門的な資料も用意しますので、安心してください。 以上

9/16 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
"A Gentle Introduction to Type Classes and Relations in Coq" の第二回目です。 予習には、以下を参考に、サンプルコードを読んでおいてください。 準備していなくても、当日、インストールから説明します。 https://github.com/suharahiromichi/doc/blob/master/coq_gitcrc.md また、上記を補足するCoqの入門的な資料も用意しますので、安心してください。 以上

8/19 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
"A Gentle Introduction to Type Classes and Relations in Coq" の第一回目です。 予習には、以下を参考に、サンプルコードを読んでおいてください。 準備していなくても、当日、インストールから説明します。 https://github.com/suharahiromichi/doc/blob/master/coq_gitcrc.md また、上記を補足するCoqの入門的な資料も用意しますので、安心してください。 以上

7/27 (木)

量子論理やりましょう。続き物ではなく単発イベントの予定です。 概要 量子論理に関する物理的文脈はさておき,数学的側面に焦点を当てたお話をします. 量子論理では,Hilbert空間の閉部分空間が命題を表現すると考えます. 2次元以上のHilbert空間の閉部分空間全体に包含関係で順序を入れると,分配律を満たさない束になります. これを量子論理と呼ぶことにします. 量子論理における命題に真理値を割り当てる関数は,二値の束準同型写像として与えられます. また,二値の束準同型写像はprime filterと呼ばれるものと対応します. 今回のお話では,束や準同型写像,filterなどの定義を確認してから,分配律と二値の束準同型写像,prime filter間の関係について概観します. そして,量子論理上には二値の束準同型写像が存在しないことを,prime filterを経由して証明します. 参考文献 ・Quantum Logic in Algebraic Approach http://www.springer.com/in/book/9780792349037

6/17 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Little Prover の 第7章。前回は7章の途中で終わりましたが、復習のために7章の最初から振り返ります。 会場はA-317に決まりました。 以上

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
the Little Prover CH8.6 から
The Little Prover の 第8章。フレーム6から始めます。 会場はA-317です。

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Little Prover の 第8章を読みます。 時間があれば第67回以降の Coq 勉強会のオリエンテーションを予定しています。

5/20 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Little Prover の 第7章。前回は7章の途中で終わりましたが、復習のために7章の最初から振り返ります。 会場はA-317に決まりました。 以上

4/15 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
今月は「完全性定理に関する勉強会」・「数学的な話題で登場する圏論に関する勉強会」に合流して開催します。 1315-1515 完全性定理 1530-1630 tannaka duality 以上 先月と場所と時間が異なりますので、注意してください。

3/18 (土)

8e4f7fce315670850c7a34f9a7813c1b ProofCafe
(開始時刻が02:30と表示されますが、14:30からです)
little prover 読書会です。 今回は 6章からです。 終了後、18:00より、よしひろさんの壮行会が予定されています。 https://proofcafe.connpass.com/event/53012/