BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//https://techplay.jp//JP
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALDESC:Coq勉強会 - (SF読み進捗ダメです会議) -  #41
X-WR-CALNAME:Coq勉強会 - (SF読み進捗ダメです会議) -  #41
X-WR-TIMEZONE:Asia/Tokyo
BEGIN:VTIMEZONE
TZID:Asia/Tokyo
BEGIN:STANDARD
DTSTART:19700101T000000
TZOFFSETFROM:+0900
TZOFFSETTO:+0900
TZNAME:JST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:628435@techplay.jp
SUMMARY:Coq勉強会 - (SF読み進捗ダメです会議) -  #41
DTSTART;TZID=Asia/Tokyo:20170820T140000
DTEND;TZID=Asia/Tokyo:20170820T180000
DTSTAMP:20260423T051923Z
CREATED:20170721T020317Z
DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/62843
 5?utm_medium=referral&utm_source=ics&utm_campaign=ics\n\n証明器Coqの
 解説書 Coq'Art を読む読書会だったのですが、まずは ソ
 フトウェアの基礎 を読むことになりました。しばらく
 は本を購入する必要はありません。Webで公開されてい
 る資料を使って勉強を進めます。\n主催者は証明器に
 ついてまったくの素人なので、基本からしっかり勉強
 する読書会にしようと思っています。「Coqって何？」
 という方は以下のリンクが参考になるかもしれません
 。\n\nプログラミング Coq\nソフトウェアの基礎 1.0.2\nCoq 
 Tutorial at Proof Summit 2011\n\n\n\n\nMoreStlc_J:\n\n\n\n\n\n* 数値\n@
 kappa\n\n\n** STLCの単純な拡張\n\n\n\n** 拡張を形式化する\n
 \n\n\n* let 束縛\n@khibino\n\n\n** STLCの単純な拡張\n\n\n\n** 拡
 張を形式化する\n\n\n\n* 対\n@nagae\n\n\n** STLCの単純な拡張
 \n\n\n\n** 拡張を形式化する\n\n\n\n* 直和\n@eldesh\n\n\n** STLC
 の単純な拡張\n\n\n\n** 拡張を形式化する\n\n\n\n* リスト\
 n@nagae\n\n\n** STLCの単純な拡張\n\n\n\n** 拡張を形式化する
 \n\n\n\n* 一般再帰\n@eldesh\n\n\n** STLCの単純な拡張\n\n\n\n** 
 拡張を形式化する\n\n\n\n* レコードとバリアント\n@khibin
 o\n\n\n** STLCの単純な拡張\n\n\n\n** 拡張を形式化する\n\n\n
 \n\nMoreStlc_J の「レコードとバリアント(Optional)」が積み
 残し。\nレコードは Records_J でやるようなので、\nバリ
 アントができたら発表します。( @khibino )\n\n\n\nReferences_
 J:\n\n\n\n\n\n定義 〜 性質\n@kappa\n\n\n参照と非停止性\n@elde
 sh\n\n\nさらなる練習問題\n( @khibino )\n\n\n\n\n\n\nSubtyping_J:\
 n\n\n\n\n\n概念\n@lion\n\n\n中核部の定義\n@lion\n\n\nサブタイ
 プ\n@lion\n\n\n型付け\n@yoshihiro503\n\n\n性質\n@yoshihiro503\n\n\n
 練習問題\n@yoshihiro503\n\n\n\n\n\n\nRecords_J:\n\n\n\n\n\n\n@nagaet\
 n\n\n\n読む順番は 章の依存関係の中心的な章 の矢印を
 追い掛けます。\nスケジュール\n開始時間は14時です\n\n
 14:00-18:00 ソフトウェアの基礎 の担当部分を発表(MoreStlc
 _J: 単純型付きラムダ計算についてさらに リスト拡張
 を入れた型保存の証明から始めます) or 各自証明\n前回
 のCoq入門講座の続き(http://www.math.nagoya-u.ac.jp/~garrigue/lect
 ure/2015_AW/index.html の第３回から)もやりたい\n\n\n18:30-20:0
 0 懇親会(有志)\n\n持ち物\n\nCoq をインストールしたノー
 トPC (ハンズオンを行なうので必ず持ってきてください
 ！)\n[https://github.com/sfja/sfja] を自分のノートPCにgit clone
 しておいてください\n全てが型付けされた世界を泳ぐ
 純粋な心\n\n集合場所\n歌舞伎座タワー 21F セミナール
 ーム\n21F に上るには 1F または B2F からエレベーターで 
 7F に上って、そこからさらに 21F に上がるエレベータ
 ーにのってください。\nslack\n気軽に質問や雑談を出来
 るように、coqtokyo.slack.com を試験運用しています。\n＠t
 miya_ @khibino @eldesh @yoshihiro503 のうちのだれかに頼んで登
 録してもらってください。( slack でアカウントとして
 利用するためのメールアドレスをお知らせください )
LOCATION:株式会社朝日ネット 会議室 東京都中央区銀座 4-1
 2-15 歌舞伎座タワー21階
URL:https://techplay.jp/event/628435?utm_medium=referral&utm_source=ics&utm
 _campaign=ics
END:VEVENT
END:VCALENDAR