圏論の、特に情報学に関係する書籍や論文の読書会です。形式は輪講形式で、聴講のみの参加もOKです。必要な背景知識としては、デカルト閉圏の定義とか、それがλ計算のモデルになってる、みたいな基本的な事がふわっと分かってれば大丈夫で、それ以上の事は都度質問があれば分かる人が説明しながら進めています。

このページでは新しい資料を読み始める時に新規参加者を募集しています。資料の途中からでも参加されたいという方はツイッターの @jun0inoue にメンション飛ばして下さい。

前回は

• J. Adámek et al., "Algebraic Theories" (https://www.cambridge.org/core/books/algebraic-theories/D6055CE69E527DE387FB557DA7264E80)

の 7.5 まで読みました。今回は 7.6 から読みます (講師 I)。

これまでに読んだもの:

• Anders Mörteberg, "Cubical Methods in Homotopy Type Theory and Univalent Foundations" (https://staff.math.su.se/anders.mortberg/papers/cubicalmethods.pdf) とそのcompanion material である証明支援系プロトタイプ (https://github.com/mortberg/cubicaltt) に付属の lecture 一通り
• Homotopy Type Theoryの教科書のめぼしい部分(http://homotopytypetheory.org/book/)
• Andrew Pitts, Relational Properties of Domains (http://www.cl.cam.ac.uk/~amp12/papers/relpod/relpod.ps.gz)
• Gordon Plotkin and Matija Pretnar, A Logic for Algebraic Effects (http://homepages.inf.ed.ac.uk/gdp/publications/Logic_Algebraic_Effects.pdf)
• Thorsten Altenkirch and Bernhard Reus, Monadic Presentations of Lambda Terms Using Generalized Inductive Types (http://www.cs.nott.ac.uk/~txa/publ/csl99.pdf)
• Gordon Plotkin and John Power, "Algebraic Operations and Generic Effects" (http://homepages.inf.ed.ac.uk/gdp/publications/alg_ops_gen_effects.pdf) [眺める程度]
• Samson Abramsky and Guy McCusker, Game Semantics (http://www.cs.cmu.edu/~jcr/gamenotes.ps.gz)
• Andrew Ker, Hanno Nickau, and Luke Ong, Innocent game models of untyped λ calculus (http://www.cs.ox.ac.uk/andrew.ker/docs/ADK01D.pdf)
• [補足資料] Luke Ong, Game Semantics and Its Applications (http://www.cs.ox.ac.uk/luke.ong/personal/talks/shell-2x2.pdf)
• Paul-André Melliès, "Functorial boxes in string diagrams" [5節まで]
• André Joyal and Ross Street, "Geometry of Tensor Calculus II" [気持ち程度]
• Jorge Sousa Pinto, "Parallel Implementation Models for the λ-Calculus Using the Geometry of Interaction"
• Samson Abramsky, Esfandiar Haghverdi, and Philip Scott, "Geometry of Interaction and Linear Combinatory Algebras"
• Abramsky and Jung, "Domain Theory" (http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf) [第2.2節のみ]
• Borceaux and Stubbe, "Short Introduction to Enriched Categories" (https://web.archive.org/web/20150907184148/http://www-lmpa.univ-littoral.fr/~stubbe/PDF/EnrichedCatsKLUWER.pdf)
• Hyland and Ong, "On Full Abstraction for PCF: I, II, and III" (https://ora.ox.ac.uk/objects/uuid:63c54392-39f3-46f1-8a68-e6ff0ec90218/datastreams/ATTACHMENT01)
• Power and Robinson, "Premonoidal Categories and Notions of Computation" (http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=F2F5668CABD327B6716EF3A3E3826E04?doi=10.1.1.23.1140&rep=rep1&type=pdf) [一部]
• Selinger, "Control Categories and Duality" (www.mathstat.dal.ca/~selinger/papers/control.pdf)
• Samson Abramsky, "Information, Processes, and Games" (https://arxiv.org/abs/1604.02603)
• Rasmus Ejlers Møgelberg and Sam Staton, "Linearly-used state in models of call-by-value" [第4節の翻訳の定義まで]
• Jeff Egger, Rasmus Ejlers Mogelberg, and Alex Simpson, "The Enriched Effect Calculus: Syntax and Semantics" (http://homepages.inf.ed.ac.uk/als/Research/Sources/eec.pdf)
• Andrea Schalk, "What is a Categorical Model for Linear Logic?" (http://www.cs.man.ac.uk/~schalk/notes/llmodel.pdf)
• G. M. Kelly, "Basic Concepts of Enriched Category Theory" (http://www.tac.mta.ca/tac/reprints/articles/10/tr10.pdf) [1.8節まで]
• Yuichi Nishiwaki, Yoshihiko Kakutani, and Yuito Murase, "Modality via Iterated Enrichment" (https://arxiv.org/abs/1804.02809)
• Stefan Forcey, "Enrichment Over Iterated Monoidal Categories" (https://arxiv.org/abs/math/0403152)
• G. A. Kavvos, "Dual-Context Calculi for Modal Logic" (https://arxiv.org/pdf/1602.04860.pdf)
• Djordje Cubric, Peter Dybjer, and Philip J. Scott, "Normalization and the Yoneda Embedding" (https://pdfs.semanticscholar.org/dc4f/878e3ac58b60da0b0ab7f63443322bbc6518.pdf)
• Thorsten Altenkirch and Jonathan Grattag, "A functional quantum programming language" (https://arxiv.org/pdf/quant-ph/0409065.pdf)
• Grattag, "A functional quantum programming language" (http://eprints.nottingham.ac.uk/10250/1/thesis.pdf)
• Milner, Parrow, and Walker, "A Calculus for Mobile Processes" (https://reader.elsevier.com/reader/sd/pii/0890540192900084?token=314F25758D6B289FAA989571D84CA0A9C1625DDD238A3525F774BCC1D7ABD7EABBC2EF316050E2360004E292902D459B)
• Cattani, Stark, and Winskel, "Presheaf models for the π-calculus" (http://homepages.inf.ed.ac.uk/stark/prempc.pdf)
• Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, "Cubical Type Theory: a constructive interpretation of the univalence axiom"
• F. William Lawvere, "Adjointness in Foundations" (https://www.jstor.org/stable/42969800)

第四十三回までのバックナンバーは partake にあったんですが、ドメインごと消えました(´ﾟдﾟ｀)

第七十七〜七十九回はページを作り忘れましたが、PintoのD論をやりました。

※Pintoの論文はどうもオンラインでは手に入らないようなので、欲しい人は言って下さい。Mackieの論文も、ACMのpaywallに阻まれているようです。