Home

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


平成26年3月17日(月)〜18日(火)
神奈川大学理学部情報科学科
第一会議室(17日)、第二会議室(18日)
〒259-1293 神奈川県平塚市土屋2946
電話 0463-59-4111(代表)
幹事 神奈川大学理学部情報科学科 木下佳樹 yoshiki@kanagawa-u.ac.jp


CSCATとは

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


プログラム

3月17日(月)

13:30 開会 (挨拶。会場、予定などの説明)
13:45-14:00 白旗優(慶応大学)
         極私的GI入門
14:05-14:35 由水輝(東京大学)
         Measurements in Proof Nets as Higher-Order Quantum Circuits
14:40-15:20 星野直彦(京都大学)
         Geometry of Interaction: From Coalgebraic Components to Algebraic Effects
15:20-15:50 休憩
15:50-16:10 角谷良彦(東京大学)
                        Towards approximate bisimulation on protocols
16:15-16:35 岡本圭史(仙台高等専門学校)
                        Title TBA
16:40-17:10 長谷川真人(京都大学)
         プログラム意味論と量子トポロジー(進捗報告)
平塚駅前へ移動
神奈川大学校舎前バス停発 17:40, (18:01), 18:27
[18:01発の便は神奈川大学バス停発着のみで神奈川大学校舎前は停車しない]
19:00 懇親会@さかなや道場平塚北口店 電話 050-5797-2917 

3月18日(火)

 9:00-10:00 蓮尾一郎(東京大学)
         Towards Coalgebraic Model Checking
10:05-10:25 小川浩志(東京大学)
         Coalgebraic Approach to Equivalences of Quantum Systems
10:30-11:00 休憩
11:00-11:15 西澤弘毅(神奈川大学)
         A sufficient condition for liftable adjunctions between
         Eilenberg-Moore categories 
11:20-11:50 卜部夏木(東京大学)
         Kleisli Simulation for Real-Weighted Automata and its Algorithm

11:55-12:25 藤井宗一郎(東京大学)

         A Categorical Approach to L-Convexity

12:25-13:30 昼食
13:30-13:45 西原秀明(産業技術総合研究所)
         Title TBA
13:50-14:20 三好博之(京都産業大学)
                        Title TBA
14:25-14:45 木下佳樹(神奈川大学)
                        形式アシュランスケースについて(これまでの仕事と今後の展望)
14:45-15:00 次回のアナウンスなど
15:00                閉会


講演の題と梗概(講演者名五十音順)

  • 卜部夏木
演題:Kleisli Simulation for Real-Weighted Automata and its Algorithm
梗概:Kleisli simulation [Hasuo, CONCUR 2006] is a generic notion that defines forward and backward simulations for various state-based systems. The existence of forward or backward simulation from one system to another implies that the trace semantics of the former system is included in the semantics of the latter. Using this framework, we implemented a program that examines whether there exists a forward or backward simulation between two real-weighted automata. We also introduce ways to modify automata so that a greater number of simulations can be found between the automata.
  • 小川浩志
演題:Coalgebraic Approach to Equivalences of Quantum Systems
梗概:The quantum branching monad Q is introduced by Hasuo and Hoshino in order to obtain denotational semantics of quantum programming language. I also use this monad Q for modeling of quantum systems or quantum protocols from a coalgebraic perspective. I'll talk about three topics from this point about quantum systems as follows: 1) trace semantics and Kleisli simulation; 2) two different notions of equivalence, namely bisimilarity and behavioral equivalence; 3) the modal logic suitable for quantum systems and expressivity results obtained from coalgebraic modal logic.
  • 岡本圭史
演題:未定
    • 角谷良彦
    演題:Towards approximate bisimulation on protocols
    梗概:For a protocol with security parameters, in order to prove its security, it may be transformed to another secure protocol such that the two protocols behave similarly except for negligible differences.  We consider a monad for approximation as a modification of the distribution monad, and discuss approximate bisimulation for such a proof method.
    • 木下佳樹
    演題:形式アシュランスケースについて(これまでの仕事と今後の展望)
    梗概:Assurance caseはシステムのassurance(安心?)に関する書類一式をいい、システムの検証(verification)の結果だけでなく、検証法やシステムへの要求の妥当性確認(validation)の結果も含むものである。アシュランスケースは形式論理を超えるものであるとされ、形式手法を適用することはできない、という見方が漫然と広がっていたが、我々はアシュランスケース等の非形式的文書の整合性検査に定理証明支援系を用いるアプローチをとる手法D-Case in AgdaをDEOSプロジェクトにおいて研究した。Formal assurance caseと呼ぶこのアプローチについて説明し、今後を展望する。武山誠との共同研究である。
    • 白旗優
    演題:極私的GI
    • 西澤弘毅
    演題:A sufficient condition for liftable adjunction's between Eilenberg-Moore categories
    梗概:We give a sufficient condition for monads P, P' and T to have an adjunction between the category of P-algebras over T-algebras and the category of P'-algebras over T-algebras.  We have three leading examples. The first one and the second one show that ideal completion gives the adjunction's between the category of join semilattices over T-algebras and the category of complete join semilattices over T-algebras for a general monad T satisfying certain distributive law.  The third leading example is an adjunction between the category of complete join semilattices and the category of pointed sets, whose right adjoint maps a complete join semilattice to its underlying set with the least element. (joint work with Hitoshi Furusawa)
      • 西原秀明
      演題:未定
        • 蓮尾一郎

        演題:Towards Coalgebraic Model Checking

        梗概:The trinity of fixed point logics, automata (on infinite objects), and games is fundamental in the current study of model checking. With the ultimate goal  being its categorical (or coalgebraic) understanding, I'll talk about our recent work on two different yet relevant aspects, namely: 1) coinductive predicates in a fibration and their construction by a final sequence; 2) generic weakest precondition semantics arising from an order-enriched monad. The former [Hasuo, Cho, Kataoka, Jacobs, MFPS 2013] is concerned about a special class of fixed point formulas (namely the greatest fixed points); and the latter [Hasuo, CMCS 2014 to appear] sets a suitable categorical domain of discourse for systems with two alternating layers of branching (such as choices by Player and Opponent in games).

        • 長谷川真人
        演題:プログラム意味論と量子トポロジー(進捗報告)
        梗概:CSCAT2010で報告した、集合と二項関係の圏Relにおける量子二重化を用いたリボンHopf代数・リボン圏の構成をきっかけとして、これまでに、プログラム意味論の文脈で量子トポロジー(量子群に由来する結び目などの不変量)の知見を応用する研究を進めてきた。研究の概要とこれまでに得られた成果を紹介するとともに、今度の発展の可能性について触れたい。
          • 藤井宗一郎
          演題:A Categorical Approach to L-Convexity
          梗概:We present an enriched-categorical approach to discrete convex analysis, a field of discrete optimization. Discrete convex analysis has been developed as a discrete version of convex analysis, transporting various notions of convex analysis to a discrete setting.  We concern L-convex sets, a discrete counterpart of convex sets. As for enriched categories, our usage of them somewhat resembles that of William Lawvere in his 1973 paper on an enriched-categorical approach to metric spaces; we mainly use as an enriching category the poset of (possibly negative) integers together with additional top and bottom elements, ordered by the opposite of the usual ordering. The main result is a Stone-type duality theorem between a class of enriched categories and that of what we call extended L-convex sets, a variant of L-convex sets. This talk is based on the speaker's bachelor thesis under the supervision of Hiroshi Hirai at the University of Tokyo.
            • 三好博之
            演題:未定
              • 星野直彦
              演題:Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects
              梗概:Girard’s Geometry of Interaction (GoI) is interaction based semantics of linear logic proofs and, via suitable translations, of functional programs in general. Its mathematical cleanness identifies essential structures  in computation; moreover its use as a compilation technique from programs to state machines―“GoI implementation,” so to speak―has been worked out by Mackie, Ghica and thers. In this paper, we develop Abramsky’s idea of resumption based GoI systematically into a generic framework that accounts for computational effects (nondeterminism, probability,  exception, global states, interactive I/O, etc.). The framework is categorical: Plotkin & Power’s algebraic operations provide an interface to computational effects; the framework is built on the  categorical axiomatization of GoI by Abramsky, Haghverdi and Scott; and, by use of the coalgebraic formalization of component calculus, we describe explicit construction of state machines as interpretations of functional programs. The resulting interpretation is shown to be sound with respect to equations between algebraic operations, as well as to Moggi’s equations for the computational lambda calculus. We illustrate the construction by concrete examples.  (Joint work with Koko Muroya and Ichiro Hasuo)
                • 由水輝
                演題:Measurements in Proof Nets as Higher-Order Quantum Circuits
                梗概:We build on the series of work by Dal Lago and coauthors and identify proof nets (of linear logic) as higher-order quantum circuits. By accommodating quantum measurement using additive slices, we obtain a comprehensive framework for programming and interpreting quantum computation.  Specifically, we introduce a quantum lambda calculus MLLqm and define its geometry of interaction (GoI) semantics--in the style of token machines--via the translation of terms into proof nets. Its soundness, i.e. invariance under reduction of proof nets, is established. The calculus MLLqm attains a pleasant balance between expressivity (it is higher-order and accommodates all quantum operations) and concreteness of  models (given as token machines, i.e. in the form of automata).


                懇親会


                参加される方は http://doodle.com/hekpappebdy7ddg3 にアクセスして
                エントリを作ってください。
                2014-03-12 22:25 現在17名参加予定です!


                日時: 3月17日19:00から

                場所: さかなや道場平塚北口店 http://r.gnavi.co.jp/g863256/

                〒254-0043 神奈川県平塚市紅谷町2-6 サクライビル2~3F
                    電話 050-5797-2917 

                会費:

                 給料とり 6000円
                 学生   3000円
                 (給料とりの学生には、どっちにするか自分で決めてもらいます。)


                神奈川大学へのアクセス

                神奈川大学理学部情報科学科のある湘南ひらつかキャンパス(平塚市土屋)へは、JR平塚駅からバスで35分、小田急秦野駅からからバス25分です。現在、「春季休業期間」の時刻表に基づいて運行されています。

                詳細は大学ホームページのここ(http://www.kanagawa-u.ac.jp/access/shonan_hiratsuka/)をご参照ください。


                参加申し込み方法

                参加される(かもしれない)方は、Subject を「CSCAT2014参加申し込み」としたメイルを、上記幹事のアドレス宛お送りください。

                講演をしてくださる方は、さらに以下の項目をお送りください。

                • 講演題目
                • 講演梗概
                • 講演者のお名前
                • 必要時間
                • 必要機器(projector以外のものが必要であれば)

                参加人数によっては部屋を小さくしたり大きくしたりする必要があるかも知れないので、参加者の概数を知りたく思います。参加を予定される方は、講演されない場合でも、上記の方法でご一報いただけるとありがたく存じます。


                周辺宿泊施設

                JR平塚駅周辺および小田急秦野駅周辺にビジネスホテルがいくつかあります。懇親会を平塚駅周辺で行う予定なので、平塚駅周辺の宿泊をお勧めします。平塚駅から秦野駅まで直行バスで40分かかります。

                平塚駅周辺の宿(ビジネスホテル)

                秦野駅周辺の宿

                過去のCSCAT

              • CSCAT 2008 (東北大学)
              • CSCAT 2004 (産総研)
              • CSCAT 2003 (慶應義塾大学)
              • Comments