本イベントについて

概要

グループMACS(後述)のTaPL分科会の定期イベントになります。

Types and Programming Languages (通称TaPL本)の基本事項を一通り理解する事を目標とします。 現時点ではイベント開催者(型理論の素人・基本的な数理的素養はあり)が毎回発表していき、聴講者が気軽に質問したり、突っ込みを入れたり、といった形式で実施しています。

型理論を初めて学ぶ参加者は、事前に流し読みをする事をお勧めしますが、予習している事は前提としません。

• TaPL本：https://www.cis.upenn.edu/~bcpierce/tapl/
• 邦訳もあるようです：https://www.ohmsha.co.jp/book/9784274069116/

発表者は原著しか所有していないため、書籍に言及する場合はそちらに準じます。ただしスライドや板書は日本語をベースとします。用語についても、邦訳と異なる可能性が高いです。

開催頻度・日時・スケジュール

現時点で毎回日時調整を行います。 開催頻度は月2~3を想定しています。

現時点で 3→5→8→9→11→15→16→23→24→26→28→29→30→31 と進む予定です。(ただし2章は都度参照)

対象者

• 型理論に興味があり、基本的な事項を知りたい方
• TaPL本を読みたい方
• 理工系大学初等年度の数学の基礎(集合・写像・述語論理学の記法とか)は抑えている方
  • 不安な方は対象書籍の2章を事前に眺める事を推奨します

必ずしも参加者の書籍保有は前提としていませんが、参照する事もあると思うので、保有をお勧めします。英語が苦手な方は邦訳もありますので、そちらご参照ください。

またこの活動の背景にあるグループの説明 https://macs.connpass.com/ についても併せてご覧ください。

注意事項

• Google Meet上で行います。
• また主催者側で、会の録画を行う事、予めご了承ください。ただし、あくまで参加できなかった方の自習用・参加した方の復習用を前提とし、問い合わせがあった関係者限定・期間限定での共有とします。
• スライド資料の共有や、スケジュール調整はDiscordで行います。

第8回の内容

間が空いたため、これまでの簡単な復習 および 11章：単純型付きlambda計算の拡張準備(できれば11.4あたりまで)

なお質問がございましたら、connpassで問い合わせしていただいて大丈夫です。

これまでの内容

• 第7回：9章：単純型付きlambda計算のCurry-Howard対応など @ 12/17
• 第6回：9章：単純型付きlambda計算の型安全性 @ 11/26
• 第5回：8章：型の導入と型安全性 @ 2022/10/29
• 第4回：5.2の拡張lambda計算-5.3 @ 2022/10/15
• 第3回：5.1-5.2のChurch encoding @ 2022/10/2
• 第2回：3.5途中-3章の終わり @ 2022/9/21
• 第1回：3.3途中-3.5途中 @ 2022/9/10
• 第0回：1章概要of概要、3.1-3.3途中 @ 2022/9/1

本グループについて

最新版は https://macs.connpass.com/ をご参照ください。

広い意味でのコンピュータ科学・情報科学を勉強・議論・習得していく、Mastering All the Computer Science (通称MACS)という活動を(最初は内輪で)始めました。

理論特化の内容(各種数理・アルゴリズム)から、応用寄りの内容(デザインパターン・DB)までの、比較的、基礎的・普遍的・汎用的な内容・側面を対象とします。逆に、機械学習のある一手法や個別のソフトウェアやライブラリの使い方といった、一過性・流行色の強いものはあまり対象としていません。

その主な活動方法としては、分科会という特定のテーマ・トピックを扱うチーム・チャンネルを立ち上げ、主催者が永遠と解説したり、持ち回りで輪読したり、議論したり、比較的自由に運営する方式を現在は実験的に採用しています。 基本的には、CSを勉強したい、という方であれば、どなたでもご参加いただけます。 ※ もちろん社会的規範等を遵守し、攻撃的な行動・発言をしなければ、という条件付きです。