ja:start

差分

このページの2つのバージョン間の差分を表示します。

この比較画面へのリンク

両方とも前のリビジョン 前のリビジョン
次のリビジョン
前のリビジョン
ja:start [2021/04/01 15:09] – [テーブル] asadaja:start [2023/10/04 12:52] (現在) – [テーブル] asada
行 45: 行 45:
  
 計算可能性理論やプログラミング言語理論の研究は形式論理学と深い繋がりがあり,当研究室も形式論理学の研究も行っています. 計算可能性理論やプログラミング言語理論の研究は形式論理学と深い繋がりがあり,当研究室も形式論理学の研究も行っています.
-形式論理学のなかでも数学の論理学的基礎を研究する数学基礎論は,伝統的には再帰理論・証明論・モデル理論・集合論に分かれ,+形式論理学のなかでも数学の論理学的基礎を研究する数学基礎論は,伝統的には再帰理論・証明論・モデル理論・集合論に分かれ,
 いずれも計算機科学と関係の深い分野ですが,なかでも証明論と計算体系の間にはCurry-Howard対応という1対1の関係が知られており, いずれも計算機科学と関係の深い分野ですが,なかでも証明論と計算体系の間にはCurry-Howard対応という1対1の関係が知られており,
 両者は不可分の関係にあります. 両者は不可分の関係にあります.
-直観主義論理体系が関数型言語のモデルである型付ラムダ計算と対応し,古典論理が第一級継続計算という大域的制御構造と対応します.+直観主義命題論理が関数型言語のモデルである型付ラムダ計算と対応し,古典命題論理が第一級継続計算という大域的制御構造を持つ型付ラムダ計算と対応します.
 また上記のプログラミング言語意味論では,再帰理論的手法・モデル理論的手法・集合論的手法が用いられることもあります. また上記のプログラミング言語意味論では,再帰理論的手法・モデル理論的手法・集合論的手法が用いられることもあります.
-近年発展が著しい型理論も論理学と計算機科学の学際領域で活発に研究されているものです.+型理論も論理学と計算機科学の学際領域で活発に研究されているものです.
 当研究室でも,その基礎理論からCoqなどの定理証明支援系まで研究を行っています. 当研究室でも,その基礎理論からCoqなどの定理証明支援系まで研究を行っています.
 また論理学に近い数学の技術として圏論というものがあり,我々の研究でもテーマによっては用いられています. また論理学に近い数学の技術として圏論というものがあり,我々の研究でもテーマによっては用いられています.
  
 ===== 研究室学生の対外発表 ===== ===== 研究室学生の対外発表 =====
 +  * 2023年03月 **菅野直孝**さん,**伊藤耀**さん,**野木知優**さんが国内研究集会[[https://jssst-ppl.org/workshop/2023/program|PPL 2023]]でポスター発表しました.
 +  * 2022年03月 **芳賀勇太**さん,**宮坂優介**さん,**上西真由**さんが国内研究集会[[https://jssst-ppl.org/workshop/2022/program|PPL 2022]]でポスター発表しました.
 +  * 2021年09月 **佐藤光**さんが国内学会[[https://jssst2021.wordpress.com/program/#ppl4_2|ソフトウェア科学会大会 2021]]で登壇発表しました.
 +  * 2021年03月 **今津徹大**さん,**佐藤光**さんが国内研究集会[[https://easychair.org/smart-program/PPL2021/|PPL 2021]]でポスター発表しました.
 +  * 2020年03月 **西山舜**さんが国内研究集会[[https://easychair.org/smart-program/PPL2020/|PPL 2020]]でポスター発表しました.
   * **2019年09月 高橋祐多さんの下記のCIAA 2019の論文がSpecial Issueに選出されました.**   * **2019年09月 高橋祐多さんの下記のCIAA 2019の論文がSpecial Issueに選出されました.**
     * **[[https://doi.org/10.1016/j.tcs.2020.12.033|これを受け更に発展させた論文]]が雑誌[[https://www.journals.elsevier.com/theoretical-computer-science|TCS]]に受理されました.**     * **[[https://doi.org/10.1016/j.tcs.2020.12.033|これを受け更に発展させた論文]]が雑誌[[https://www.journals.elsevier.com/theoretical-computer-science|TCS]]に受理されました.**
行 63: 行 68:
   * 2018年10月 **阿部和敬**さん,**小澤祐也**さん,**高橋祐多**さんが国内研究集会[[https://sigpro.ipsj.or.jp/pro2018-3/program/|PRO 2018(3)]]で登壇発表しました.   * 2018年10月 **阿部和敬**さん,**小澤祐也**さん,**高橋祐多**さんが国内研究集会[[https://sigpro.ipsj.or.jp/pro2018-3/program/|PRO 2018(3)]]で登壇発表しました.
  
 +===== 出版論文 =====
 +^ 論文DL                                                    ^ 出版年   ^ 論文タイトル                                                                                 ^ 著者名                                                                                                                     ^ 雑誌・会議名                                                                                                                          ^
 +|                                                         | 2023  | Compositional Probabilistic Model Checking with String Diagrams of MDPs                | Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo                                                      | [[http://www.i-cav.org/2023/|Computer Aided Verification (CAV 2023)]]                                                           |
 +| [[https://doi.org/10.1007/978-3-031-19135-0_8|doi]]     | 2022  | On Higher-Order Reachability Games vs May Reachability                                 | Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi                                                                       | [[https://rp2022.mpi-sws.org/index.html|Reachability Problems (RP 2022)]]                                                       |
 +| [[https://dl.acm.org/doi/10.1145/3531130.3533373|doi]]  | 2022  | Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings  | Takeshi Tsukada and Kazuyuki Asada                                                                                      | [[https://lics.siglog.org/lics22/index.php|Logic in Computer Science (LICS 2022)]]                                              |
 +| [[https://doi.org/10.4204/EPTCS.351.17|doi]]            | 2021  | A Compositional Approach to Parity Games                                               | Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo                                                      | [[https://www.coalg.org/calco-mfps2021/|Mathematical Foundations of Programming Semantics (MFPS 2021)]]                         |
 +| [[https://doi.org/10.4230/LIPIcs.MFCS.2021.79|doi]]     | 2021  | Idempotent Turing Machines                                                             | Keisuke Nakano                                                                                                          | [[https://compose.ioc.ee/mfcs/|Mathematical Foundations of Computer Science (MFCS 2021)]]                                       |
 +| [[https://doi.org/10.1007/978-3-030-79837-6_11|doi]]    | 2021  | A Tangled Web of 12 Lens Laws                                                          | Keisuke Nakano                                                                                                          | [[https://reversible-computation-2021.github.io/|Reversible Computation (RC 2021)]]                                             |
 +| [[https://doi.org/10.1007/978-3-030-52482-1_3|doi]]     | 2020  | Involutory Turing Machines                                                             | Keisuke Nakano                                                                                                          | [[https://reversible-computation-2020.github.io/|Reversible Computation (RC 2020)]]                                             |
 +| [[https://doi.org/10.23638/LMCS-16(2:8)2020|doi]]       | 2020  | On properties of B-terms                                                               | Mirai Ikebuchi and Keisuke Nakano                                                                                       | Logical Methods in Computer Science                                                                                             |
 +| [[https://doi.org/10.4230/LIPIcs.FSCD.2020.22|doi]]     | 2020  | Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars   | Kazuyuki Asada and Naoki Kobayashi                                                                                      | [[https://fscd2020.org/|Formal Structures for Computation and Deduction (FSCD 2020)]]                                           |
 +| [[https://doi.org/10.4230/LIPIcs.FSCD.2020.21|doi]]     | 2020  | On Average-Case Hardness of Higher-Order Model Checking                                | Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada                                    | [[https://fscd2020.org/|Formal Structures for Computation and Deduction (FSCD 2020)]]                                           |
 +| [[https://doi.org/10.1016/j.tcs.2020.12.033|doi]]       | 2020  | Streaming Ranked-Tree-to-String Transducers                                            | Yuta Takahashi, Kazuyuki Asada, and Keisuke Nakano                                                                      | Theoretical Computer Science                                                                                                    |
 +| [[https://doi.org/10.1007/978-3-030-23679-3_19|doi]]    | 2019  | Streaming Ranked-Tree-to-String Transducers                                            | Yuta Takahashi, Kazuyuki Asada, and Keisuke Nakano                                                                      | [[https://im.saske.sk/ciaa2019/|Implementation and Application of Automata (CIAA 2019)]]                                        |
 +| [[https://doi.org/10.1109/BIGCOMP.2019.8679145|doi]]    | 2019  | Toward BX-based Architecture for Controlling and Sharing Distributed Data              | Yasunori Ishihara, Hiroyuki Kato, Keisuke Nakano, Makoto Onizuka, and Yuya Sasaki                                       | [[http://www.prg.nii.ac.jp/projects/biscuits/second-workshop/|Software Foundations for Data Interoperability (SFDI 2019)]]      |
 +| [[https://doi.org/10.1109/BIGCOMP.2019.8679236|doi]]    | 2019  | Flexible framework for data integration and update propagation: system aspect          | Yasuhito Asano, Dennis-Florian Herr, Yasunori Ishihara, Hiroyuki Kato, Keisuke Nakano, Makoto Onizuka, and Yuya Sasaki  | [[http://www.prg.nii.ac.jp/projects/biscuits/second-workshop/|Software Foundations for Data Interoperability (SFDI 2019)]]      |
 +| [[https://doi.org/10.4230/LIPIcs.FSTTCS.2018.14|doi]]   | 2018  | Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered                         | Kazuyuki Asada and Naoki Kobayashi                                                                                      | [[https://www.fsttcs.org.in/archives/2018/|Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)]]  |
 +| [[https://doi.org/10.4230/LIPIcs.FSCD.2018.18|doi]]     | 2018  | On repetitive right application of B-terms                                             | Mirai Ikebuchi and Keisuke Nakano                                                                                       | [[https://www.cs.le.ac.uk/events/fscd2018/|Formal Structures for Computation and Deduction (FSCD 2018)]]                        |
 +| [[https://doi.org/10.11309/jssst.35.52|doi]]            | 2018  | 木から文字列への決定性トップダウン変換の等価性判定アルゴリズムの実用性について                                                | 高橋 祐多, 中野 圭介                                                                                                            | コンピュータ ソフトウェア                                                                                                                   |
  
 ===== メンバー ===== ===== メンバー =====
  
-^ 役職    ^ 名前                                               ^ Name               ^ Email                                 +^ 役職          ^ 名前                                                 ^ Name                ^ Email (+ <-> @)                      
-| 教授    | [[https://www.riec.tohoku.ac.jp/~ksk/|中野 圭介]]    | NAKANO Keisuke     | ksk + @riec.tohoku.ac.jp              | +| 教授          | [[https://www.riec.tohoku.ac.jp/~ksk/|中野 圭介]]    | NAKANO Keisuke      | ksk + riec.tohoku.ac.jp              | 
-| 助教    | [[https://www.riec.tohoku.ac.jp/~asada/|浅田 和之]]  | ASADA Kazuyuki     | asada + @riec.tohoku.ac.jp            | +| 助教          | [[https://www.riec.tohoku.ac.jp/~asada/|浅田 和之]]  | ASADA Kazuyuki      | asada + riec.tohoku.ac.jp            
-| 修士課程  今津 徹大                                            IMAZU Tetsuhiro    t-imazu @riec.tohoku.ac.jp          +| :::           | [[https://kentaro-kikuchi.github.io/|菊池 健太郎]]   | KIKUCHI Kentaro     | kentaro.kikuchi + riec.tohoku.ac.jp  
-| :::   佐藤 光                                             SATO Akira         akira_sato @riec.tohoku.ac.jp       +| 修士課程      上西 真由                                            UENISHI Mayu        mayu0802 + riec.tohoku.ac.jp         
-| :::   眞田 耕太                                            SANADA Kota        kotas @riec.tohoku.ac.jp            | +| :::           菅野 直孝                                            KANNO Naotaka       naotaka + riec.tohoku.ac.jp          
-| :::   芳賀勇太                                             HAGA Yuta          hayu1176 @riec.tohoku.ac.jp         +| :::           伊藤 耀                                              ITO Yo              yoito + riec.tohoku.ac.jp            | 
-| :::   宮坂介                                             MIYASAKA Yusuke    miya4423 @riec.tohoku.ac.jp         +| :::           中村 卓武                                            NAKAMURA Takumu     takumu + riec.tohoku.ac.jp           
-| 学士課程  石鉢健太                                             ISHINOHACHI Kenta  kenta.ishinohachi.r8@dc.tohoku.ac.jp  +| :::           野木 知優                                            NOGI Chihiro        nogi + riec.tohoku.ac.jp             
-| :::   上西真由                                             UENISHI Mayu       mayu.uenishi.p6@dc.tohoku.ac.jp       +| 学士課程      齋藤 佑貴                                            SAITO Yuki          yuki1226 + riec.tohoku.ac.jp         
-:::                                                                                                             |+| :::           橋場 慧志                                            HASHIBA Keishi      hashibak + riec.tohoku.ac.jp         
 +特別研究学生  許 兆恒                                              HUA Xiu-Heng Kevin  xhua + riec.tohoku.ac.jp             | 
  
 OB: OB:
-  * 2020年:西山 舜(修士)+  * 2023年:芳賀 勇太(修士),宮坂 優介(修士),石鉢 健太(学士) 
 +  * 2022年:佐藤 光(修士) 
 +  * 2021年:今津 徹大(修士) 
 +  * 2020年:西山 舜(修士),眞田 耕太(学士)
   * 2019年:阿部 和敬(修士),小澤 祐也(修士),高橋 祐多(修士)   * 2019年:阿部 和敬(修士),小澤 祐也(修士),高橋 祐多(修士)
 ===== リンク ===== ===== リンク =====
  • ja/start.1617257376.txt.gz
  • 最終更新: 2021/04/01 15:09
  • by asada