理論計算機科学と圏論ワークショップ

CSCAT 2019

CSCAT とは

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

参加申し込み方法

講演を希望される方、懇親会へ参加を希望される方は2月22日（金）までにそれぞれ申し込みフォームへご記入下さい。講演のみ申し込みを引き続き受け付けています。聴講のみで懇親会にも参加されない場合は申し込み不要です。

懇親会

プログラム

3月9日

  • 13:55- オープニング
  • 14:00- 勝股 審也（国立情報学研究所）
  • 14:30- 岡本 圭史（仙台高等専門学校）
  • 15:30- 安部 達也（千葉工業大学）
  • 16:30- 丸山 善宏（京都大学）

3月10日

  • 10:30- 浦本 武雄 （東北大学）
  • 13:00- 松田 一孝 （東北大学）
  • 14:00- 荒武 永史 （京都大学）

講演タイトル・概要

  • 勝股 審也（国立情報学研究所）「A Double-Category Theoretic Analysis of Graded Linear Exponential Comonads」
    • Abstract: Graded linear exponential comonads are a graded extension of linear exponential comonads, and provide a categorical semantics of resource-sensitive exponential modality in linear logic. In this paper, we propose a concise double-category theoretic formulation of graded linear exponential comonads as a kind of monoid homomorphisms from the multiplicative monoids of semirings to the composition monoids of symmetric monoidal endofunctors. We also exploit this formulation to derive the category of graded comonoid-coalgebras, which decompose graded linear exponential comonads into symmetric monoidal adjunctions plus twists.
  • 岡本 圭史（仙台高等専門学校）「Enumerating Dung's Extensions with an SMT Solver」
  • 安部 達也（千葉工業大学） 「対称ラムダ計算の双側面的解釈」
  • 丸山 善宏（京都大学）「Harmony, Higher-Order Rules, and the Curry-Howard-Lambek Correspondence」
    • Abstract: Different instances of Curry-Howard-Lambek correspondence have been developed; yet a general mechanism underpinning them is still unclear. Building upon the theory of higher-order rules in proof-theoretic semantics, we explicate a uniform mechanism to derive from logical constants the corresponding categorical constructions, and thereby establish the universal logic-category correspondence on the basis of general-elimination harmony (GE-harmony for short). This means that general-elimination harmony entails the Curry-Howard-Lambek correspondence: any logical constants harmoniously definable within the system of higher-order rules can in principle be given categorical semantics. We also have a look at several examples of this general mechanism, one of which is a contradictory constant as in the liar paradox, corresponding to certain "liar categories." Since not all logical constants defined via GE harmony come from adjoint situations, we also compare GE harmony with Lawverian categorical harmony. To this end, we revist the idea of structural functors by Kosta Dosen, which allows us to revise and sharpen Lawverian harmony. We then consider how many of GE-harmonious logical constants come from categorical adjunctions, or how many of them are categorically harmonious as well.
  • 浦本 武雄 （東北大学） 「類体論について」
  • 松田 一孝 （東北大学） 「Sparcl: A Language for Partially-Invertible Computation」
  • 荒武 永史 （京都大学）「モデル理論におけるガロア理論的現象の圏論的解釈について」


過去の CSCAT