keigoi (@keigoi)


参加する勉強会

4/21 (土)


名古屋大学 多元数理科学棟　307教室 名古屋市千種区不老町
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 インストール方法などについての質問も常に歓迎です。 以上


過去の勉強会

2/17 (土)


名古屋大学 多元数理科学棟　307教室 名古屋市千種区不老町
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 インストール方法などについての質問も常に歓迎です。 以上

2/9 (金)


名古屋大学 東山キャンパス 情報学研究科棟 8F 802号室 名古屋市千種区不老町
概要 Martin-Loefの型理論とか勉強しましょう。 第4回は以下の文献などを参考にdirected type theoryをやります http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf https://tel.archives-ouvertes.fr/tel-01590515/document http://www.lsv.fr/~dubut/defense.pdf 計画 第一回 intensional / extensional type theory 第二回 universe 第3回 cubical type theory 第4回 directed type theory 第?回 observational type theory

1/20 (土)


名古屋大学 多元数理科学棟　307教室 名古屋市千種区不老町
8e4f7fce315670850c7a34f9a7813c1b ProofCafe
今回（72回）から、Software Foundations から、型付ラムダの章と、Hoare論理の章を読んでいく予定です。 その他の今後予定されるテーマについては、以下を参照してください。 これを取り上げて欲しい、という意見は常に歓迎しています。 https://sites.google.com/site/suharahiromichi/themas 以上

1/17 (水)


来栖川電算 名古屋市中区新栄1丁目29-23 アーバンドエル新栄2階
50a44fe02b59d3bb9a33132348195c8f Sicss Society Public Seminars & Workshops
証明中心でピアスの型システム入門を読む会
内容 TaPL (型システム入門) をみんなで読みましょう。 実装はあまりやらずに主に証明を中心に読み進めます。 今回 今回は3章から 持ち物 型システム入門 （無ければ隣の人に見せてもらえるかも） 参加枠について "Sicss Society枠"はサークル関係者のための枠です。 よくわからない方は一般枠からお申し込みください

12/2 (土)


世界のビール博物館　大名古屋ビルヂング店 愛知県 名古屋市中村区 名駅 3-28-12 大名古屋ビルヂング ps & Restaurants ３F
065d9c3a04fcc72e941b60c63551da0e NGK2017B
夜の部（大忘年会）の募集ページです。参加費は調整中です。 NGK2017Bの詳細は、 http://ngk2017b.connpass.com/ をご覧ください。

11/25 (土)


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

11/9 (木)


Misoca 愛知県名古屋市中村区名駅2丁目35番22号 メビウス名古屋ビル2階
概要 Martin-Loefの型理論とか勉強しましょう。 （第2回はuniverseの話に費やしたので）第3回は Cohen et al., Cubical Type Theory: a constructive interpretation of the univalence axiom https://arxiv.org/abs/1611.02108 を参考にcubical type theoryをやります。以下の実装も触る予定です。 https://github.com/mortberg/cubicaltt 計画 第一回 intensional / extensional type theory 第二回 universe 第3回 cubical type theory 第?回 observational type theory 第?回 2-dimensional type theory

10/25 (水)


Misoca 愛知県名古屋市中村区名駅2丁目35番22号 メビウス名古屋ビル2階
概要 Martin-Loefの型理論とか勉強しましょう。 第2回は Cohen et al., Cubical Type Theory: a constructive interpretation of the univalence axiom https://arxiv.org/abs/1611.02108 を参考にcubical type theoryをやります。以下の実装も触る予定です。 https://github.com/mortberg/cubicaltt 計画 第一回 intensional / extensional type theory 第二回 cubical type theory 第三回 observational type theory

10/5 (木)


Misoca 愛知県名古屋市中村区名駅2丁目35番22号 メビウス名古屋ビル2階
概要 Martin-Loefの型理論とか勉強しましょう。 第一回は Hofmann, "Extensional concepts in intensional type theory" http://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/ を参考にしつつ、intensional / extensional type theoryのコア部分をやります。 動く実装があればそれも試すかも 計画 第一回 intensional / extensional type theory 第二回 observational type theory 第三回 cubical type theory

9/17 (日)


来栖川電算 名古屋市中区新栄1丁目29-23 (アーバンドエル新栄2階)
台風18号について 台風18号の接近に伴い、17日15時以降名古屋が暴風域に入る可能性があります。 したがって開催時間をはやめ、11:00から14:00くらいに変更します。 作って食べる料理は夕食ではなく昼食となります。 Talkの時間割も変更になると思いますが、現地で決定します。 概要 お茶と料理を楽しみながら関数プログラミングの話とかしましょう。 TOC(台風による予定変更前の内容) 14:00-15:00 Talk 1　依存型の話 (@t6s) 15:00-16:00 お茶 & Talk 2 数学者のいう美しさってなんじゃらほい (@tannakaken) 16:00-17:00 Talk 3　OCaml で線形型を使ったプログラミングの話 (@keigoi) 17:30-20:30 料理と夕食 & Talk 4 分割数の話 (@wasajifu1) お茶 台湾茶 (@GregWeng) 抹茶 (@t6s) 料理 沙茶料理 (@GregWeng) その他 淹れたいお茶などの持ち込み歓迎します

5/20 (土)


名古屋大学 理学部A棟 A-317教室 名古屋市千種区不老町
8e4f7fce315670850c7a34f9a7813c1b ProofCafe
The Little Prover の 第7章。前回は7章の途中で終わりましたが、復習のために7章の最初から振り返ります。 会場はA-317に決まりました。 以上

5/11 (木)


Misoca 愛知県名古屋市中村区名駅2丁目35番22号 メビウス名古屋ビル2階
概要 HFと有限の世界を勉強しましょう。 第7回は[1]のIV.5.9、第一不完全性定理のあたりを読みます. 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST III章 III pp.273- 有限主義 IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.3 pp.313- 構文のencoding ... (この辺未定; [2]も参照しつつやる) IV.5.32 第二不完全性 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346

4/20 (木)


Misoca 愛知県名古屋市中村区名駅2丁目35番22号 メビウス名古屋ビル2階
概要 HFと有限の世界を勉強しましょう。 第6回は[1]の IV.3.11のあたりを読みます. 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST III章 III pp.273- 有限主義 IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.3 pp.313- 構文のencoding ... (この辺未定; [2]も参照しつつやる) IV.5.32 第二不完全性 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346

4/15 (土)


名古屋大学 多元数理研究科555教室 名古屋市千種区不老町
8e4f7fce315670850c7a34f9a7813c1b ProofCafe
今月は「完全性定理に関する勉強会」・「数学的な話題で登場する圏論に関する勉強会」に合流して開催します。 1315-1515 完全性定理 1530-1630 tannaka duality 以上 先月と場所と時間が異なりますので、注意してください。

3/29 (水)


Misoca 愛知県名古屋市中村区名駅2丁目35番22号 メビウス名古屋ビル2階
概要 HFと有限の世界を勉強しましょう。 第5回は[1]の IV.3.9, IV.3.11のあたりを読みます. 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST III章 III pp.273- 有限主義 IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.3 pp.313- 構文のencoding ... (この辺未定; [2]も参照しつつやる) IV.5.32 第二不完全性 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346

3/18 (土)


名古屋大学 A317教室 名古屋市千種区不老町
8e4f7fce315670850c7a34f9a7813c1b ProofCafe
（開始時刻が02:30と表示されますが、14:30からです）
little prover 読書会です。 今回は 6章からです。 終了後、18:00より、よしひろさんの壮行会が予定されています。 https://proofcafe.connpass.com/event/53012/