CSCAT 2025＠崇城大学

理論計算機科学と圏論ワークショップ
Computer Science and Category Theory

NEWS: 3/11: CSCAT2025は無事に閉会しました。 3/6: 集会プログラムを掲載しました。 3/4:バス・電車の時刻表と懇親会情報を掲載しました。 3/1:参加・講演申し込みを〆切りました。以降は参加登録のみ受け付けますので、下記幹事連絡先にメールお願いします。1/30:初日の午前に議論セッションの予定を追加しました。1/28: サイトを公開しました。

概要

CSCATとは

CSCAT（理論計算機科学と圏論ワークショップ）は、数学の分野である圏論の情報科学への応用に関心を持つ研究者による研究集会です。 通常の学会では、時間の制約などのため研究の詳細にまで立ち入った発表と議論はなかなかむずかしいのが実情です。 本研究集会は、１つ１つの発表に長い時間を割り当て、じっくりと話を聞き議論する場を提供することを目的としています。


アクセス

崇城大学公式サイト内アクセス, キャンパスマップ
JR鹿児島本線「崇城大学前」駅, 九州産交バス「崇城大学前」バス停より徒歩5分以内

バス時刻表

JR時刻表


参加登録・発表申し込み（2月28日〆切）

Googleフォームからの参加・講演申し込みは〆切りました。以降は参加登録のみ受け付けますので、幹事にメール連絡をお願いします。


懇親会

1日目（3/10）の夜に予定しています。場所は未定（熊本市中心部？）。上記参加登録フォームからお申し込みください。懇親会の参加表明は後日でも大丈夫です。2/28までにフォームへの回答を編集してください。懇親会の受付は終了しました。申し込まれた方でもし変更が生じましたら幹事までご連絡ください。

懇親会は19:15から開始します。大学から直接懇親会場に移動する場合は大学から徒歩でバス停「上熊本営業所」に向かい、そこからバスで「市役所前」に移動します。市役所前から会場までは徒歩6分程度です。
魚河岸 番屋
上熊本営業所時刻表


プログラム

PDF版はこちら

3 月 10 日（月）

09:30–10:30 受付・議論セッション
10:30–11:15 上村 太一（名古屋大学） An elementary definition of opetopic sets Slides
11:15–12:00 今田 慧（コーネル大学・国立情報学研究所） A Nonstandard Temporal Logic for Continuous-Time Verification
12:00–13:00 昼食休憩
13:00–13:45 中村 卓武（東北大学） 深層学習アルゴリズムの関手的構成の圏論的定式化 Slides
13:45–14:30 Sori Lee, Strict bilimits Slides
14:30–14:45 休憩
14:45–15:30 奈須 隼大（京都大学） Cartesian Equipments and Cartesian Bicategories: Categorical Logic Meets Double Categories- Side B Slides
15:30–16:15 河瀬 悠人（京都大学） Double categories of profunctors Slides
16:15–16:30 休憩
16:30–17:00 星野 恵佑（京都大学） Bivirtual double categories and localisation of composing cells Slides
17:00–17:30 モンタキュート・ヨアフ（国立情報学研究所・ケンブリッジ大学） 有限モデル理論における圏論的手法
17:30-18:30 自由討論
19:15 懇親会

3 月 11 日（火）

09:30–10:00 池田 侑登（東京大学） A categorical approach to Gödel’s incompleteness via arithmetic universes Slides
10:00–10:45 米田 豊（京都大学） Nonstandardization of hyperdoctrines: from filters to watchtowers
10:45–11:00 休憩
11:00–11:45 佐原 悠太（京都産業大学） 因果構造と統計的因果推論に関する圏論的モデル Slides
11:45–12:45 昼食休憩
12:45–13:15 佐藤 玄基, Presentation of finite Reedy categories as localizations of finite direct categories Slides
13:15–14:00 前原 悠究（京都大学） Upgrading an equivalence to an adjoint equivalence, but in dimension ω Slides
14:00–14:15 休憩
14:15–15:00 洞 龍弥（東京大学） Topoi of automata Slides
15:00–15:45 谷口 雅弥（理化学研究所） 範疇文法と自由コンパクト2圏
15:45 閉会

ポスター発表

西宮 優作（理化学研究所 AIP） Complexity and structure of non-commutative multiplicative Linear Logic via computational, algebraic and categorical models
平田 賢吾（エディンバラ大学） 量子スイッチのための高階プログラミング言語の線形論理による型付け
眞田 嵩大（福井県立大学 情報センター） ニューラルネットワークプログラミング言語のための代数構造

講演概要

上村 太一（名古屋大学）
Title: An elementary definition of opetopic sets
Abstract: We propose simple structure-axiom style definitions of opetopes and opetopic sets. We show that our definition is equivalent to an existing one in the literature.
今田 慧（コーネル大学・国立情報学研究所）
Title: A Nonstandard Temporal Logic for Continuous-Time Verification
Abstract: Methods for verifying temporal properties are widely used in program verification, where the notion of time is inherently discrete. In contrast, verification methods for continuous-time systems remain less developed. We present a novel approach to verify temporal properties of continuous-time systems using the theory of infinitesimals. In our method, continuous-time traces are modeled as discrete-time traces with infinitesimal timesteps. To specify our properties, we introduce a fragment of linear temporal logic (LTL) with both discrete and continuous time semantics, and prove a preservation theorem to reduce temporal verification of continuous-time traces to that of discrete-time traces.
To demonstrate our method, we introduce a fragment of WHILE-dt, an imperative programming language with infinitesimals, and define a continuous-time trace semantics constructed using discrete-time traces. We develop a proof system to verify temporal properties of WHILE-dt programs, using classical verification ideas like loop invariants and ranking functions. We show the effectiveness of our approach by verifying temporal properties of several hybrid systems modeled in WHILE-dt. To aid in verification, we also provide a prototype implementation for checking safety and liveness properties of WHILE-dt programs.
中村 卓武（東北大学大学院情報科学研究科）
Title: 深層学習アルゴリズムの関手的構成の圏論的定式化
Abstract: 本発表ではFongらが提唱した、関手による深層学習アルゴリズムの構成をより洗練させる。具体的にはその関手のill-definednessを修正し、関手性を維持しつつ、機械学習における汎用性を高める。
Sori Lee
Title: Strict bilimits
Abstract: In the context of 2-categories and 2-functors, the notion of (weighted) limits diversifies into strict/pseudo/lax/oplax limits/bilimits. These notions are not disjoint; in fact, they constitute a hierarchy, with some subsuming others. Curiously, the literature appears silent on strict bilimits, despite the fact that they are the most general one among these notions. Instead, authors discuss strict limits and bilimits (= pseudobilimits), which are the two apex notions when strict bilimits are not considered. This leads to the question of whether strict bilimits are a superfluous notion. I'll describe an elementary construction that produces examples of a 2-category that has strict biequalisers but not strict equalisers. Since bilimits don't admit strict biequalisers, this confirms that strict bilimits are not subsumed by bilimits and strict limits.
奈須 隼大（京都大学）
Title: Cartesian Equipments and Cartesian Bicategories: Categorical Logic Meets Double Categories- Side B
Abstract: Cartesian bicategories, introduced by Carboni and Walters, form a class of bicategories in which one can take "finite products." Typical examples of those products include the direct products of sets in the bicategory Rel of sets and relations, and the product categories in the bicategory Prof of categories and profunctors. However, they do not coincide with the actual (bi)products in those bicategories, as those products do not possess the same universal property for relations or profunctors as for functions or functors. This discrepancy leads to the intricate formulation of cartesian bicategories.
In this talk, I will introduce cartesian equipments, a certain class of double categories introduced by Aleiferi, and explain in what sense they provide a more natural framework than cartesian bicategories and still cover most of the examples studied in terms of cartesian bicategories. I will then focus on a specific subclass of cartesian equipments that closely resemble Rel as a cartesian equipment.
This talk is based on my master's thesis (https://arxiv.org/abs/2501.17869).
河瀬 悠人（京都大学数理解析研究所）
Title: Double categories of profunctors
Abstract: Enriched categories have been considered as a variation of category theory. From the viewpoint of formal category theory, it is natural to consider not only enriched functors but also enriched profunctors as morphisms between enriched categories. These form a double-categorical structure called virtual double categories. In the talk, I will give a characterization of such virtual double categories of enriched categories via "versatile colimits," which is a new notion of double-categorical colimits. This characterization is strict in the sense that it is up to equivalence between virtual double categories and, at the level of objects, up to isomorphism of enriched categories. Throughout the talk, I will treat enrichment in a unital virtual double category rather than in a bicategory or a monoidal category.
星野 恵佑（京都大学）
Title: Bivirtual double categories and localisation of composing cells
Abstract: A virtual double category generalizes multicategories to a many-object context. We introduce bivirtual double categories, which similarly extend coloured PROs and allow string diagram representations for double categories. While many double categories (e.g., Span, Mod) arise from (co)virtual double categories where every path is composable, not all virtual double categories become double categories. In such cases, “cells” whose codomains are composable paths can only be discussed indirectly via universality conditions. To address this, we construct, from a virtual double category X and a suitable collection C of strongly opcartesian cells, a bivirtual double category X/C along with an embedding X→X/C that inverts the cells in C. This framework provides a diagrammatic method to directly handle cells with composable paths as their codomains, even in virtual double categories that do not becomes double categories.
モンタキュート・ヨアフ（国立情報学研究所・ケンブリッジ大学）
Title: 有限モデル理論における圏論的手法
Abstract: 近年、圏論的手法は有限モデル理論と組合せ論における結果の一般化において重要な役割を果たしてきました。本発表ではその基本的な考え方を紹介し、最近の成果をいくつか概観します。
池田 侑登（東京大学大学院数理科学研究科）
Title: A categorical approach to Gödel’s incompleteness via arithmetic universes
Abstract: In the 1970s, Joyal provided a categorical interpretation of Gödel’s incompleteness theorems in his lecture, introducing certain categories called “arithmetic universes”. Although this approach would offer a structural perspective on self-referential concepts in logic, such as incompleteness, Joyal’s insights were never formally published and have remained largely unexplored. In this talk, we present our attempt to reconstruct and refine his proof and discuss the applicability of Joyal’s idea.
米田 豊（京都大学 理学研究科）
Title: Nonstandardization of hyperdoctrines: from filters to watchtowers
Abstract: Palmgren presents a sheaf‑theoretic approach to the constructive nonstandardization of the category of sets using filter bases. However, little progress has been made in extending this method to more general theories—here understood as first‑order hyperdoctrines. In this talk, we introduce a method that, from any first‑order hyperdoctrine satisfying appropriate conditions, yields a nonstandardization that is itself a first‑order hyperdoctrine. Our approach departs from his filter‑based framework by replacing filters with a more intricate structure—a "watchtower." This new concept is motivated by a detailed reexamination and reconfiguration of Palmgren's construction.
佐原 悠太（京都産業大学大学院）
Title: 因果構造と統計的因果推論に関する圏論的モデル
Abstract: TBA
佐藤 玄基
Title: Presentation of finite Reedy categories as localizations of finite direct categories
In this talk, we present a novel construction that, for a given Reedy category $C$, produces a direct category $\operatorname{Down}(C)$ and a functor $\operatorname{Down}(C) \to C$, exhibiting $C$ as an $(\infty,1)$-categorical localization of $\operatorname{Down}(C)$. This result refines previous constructions in the literature by ensuring that $\operatorname{Down}(C)$ is finite whenever $C$ is finite—a property not guaranteed by existing approaches, such as those by Lurie or by Barwick and Kan.
As an intended future application, this finiteness property is expected to be useful for embedding the construction into the syntax of a (non-infinitary) logic. In particular, the author expects that the construction may be used to develop a meta-theory of finitely truncated simplicial types and other finite Reedy presheaves for homotopy type theory, thereby extending Kraus and Sattler's unfinished approach.
This talk is based on arXiv:2502.05096.
前原 悠究（京都大学数理解析研究所）
Title: Upgrading an equivalence to an adjoint equivalence, but in dimension ω
Abstract: It is well known that any equivalence of categories, or more generally any equivalence in a 2-category, can be upgraded to an adjoint equivalence. I will talk about a counterpart of this result in the context of weak ω-categories. This talk is based on joint work with Soichiro Fujii (Masaryk University) and Keisuke Hoshino (Kyoto University).
洞 龍弥（東京大学）
Title: Topoi of automata
Abstract: Grothendieckは，有限的/離散的な対象である整数論に対して連続的な幾何学の手法を持ち込むため，toposを定義しました．Topos，少なくともその表示であるsite，は現代の整数論の基本的な道具となっています．
オートマトンや正則言語の理論も有限的/離散的な組合せ論ですが，ここに連続的な幾何学の手法を持ち込むことは可能でしょうか．例えば，正則言語の情報を全て持った空間(= topos)を構成し，その空間の点，部分空間，商空間，局所連結性，コホモロジー，基本群について語ることは可能でしょうか．
この発表では，「正則言語の空間」を一つ構成し，その種々の表示/性質について紹介します．発表は，「Topoi of automata I」 https://arxiv.org/abs/2411.06358 と現在進行中の「Topoi of automata II」を元にしています．
谷口 雅弥（理化学研究所）
Title: 範疇文法と自由コンパクト2圏
Abstract: J. Lambek は、数理論理学の分野でLambek 計算 という部分構造論理の基礎となる論理体系をつくったことで知られている。 この Lambek 計算は数理言語学にモチベーションを持ち 範疇文法という文法体系を数学的に捉えること狙った試みであった。 Lambek は何度かこの範疇文法に対して圏論的解釈を与えることに挑戦している。 前回のCSCATで Lambek が体系を圏論的解釈した最初の試みついて紹介した。今回はその続きとして範疇文法とくに Pregroup 文法に対する自由コンパクト2圏を用いた圏論的解釈の試み紹介する。

過去のCSCAT