Sekiyama Taro 関山太朗

Researcher Number	80828476
Other IDs
Affiliation (Current)	2025: 国立情報学研究所, アーキテクチャ科学研究系, 准教授
Affiliation (based on the past Project Information) *help	2022 – 2025: 国立情報学研究所, アーキテクチャ科学研究系, 准教授 2019 – 2022: 国立情報学研究所, アーキテクチャ科学研究系, 助教
Review Section/Research Field	Principal Investigator Basic Section 60050:Software-related / Medium-sized Section 60:Information science, computer engineering, and related fields Except Principal Investigator Medium-sized Section 60:Information science, computer engineering, and related fields / Basic Section 60050:Software-related / Broad Section J
Keywords	Principal Investigator 型システム / プログラミング言語 / 時相的検証 / 計算効果 / 代数的効果ハンドラ / 並行・並列プログラム / プログラム検証 / 形式検証 / 漸進的型システム / 継続渡し形式 / レコード / 多相性 / 漸進的型付け … More Except Principal Investigator … More プログラム検証 / 機械学習 / 人工知能 / ソフトウェア / 形式検証 / システム検証 / CHCソルバ / 定理自動証明 / 演繹的推論 / ソフトウエア契約 / ソフトウェア契約 / 相互運用性 / プログラミング言語 / 高階不動点論理 / 高階モデル検査 / 深層学習 / ホーン節ソルバ / 定理証明 / 制約付きホーン節 / 自動証明 / 強化学習 Less

AIを含むソフトウェアのための形式検証手法
- Principal Investigator
  
  末永幸平
- Project Period (FY)
  2025 – 2029
- Research Category
  
  Grant-in-Aid for Scientific Research (A)
- Review Section
  
  Medium-sized Section 60:Information science, computer engineering, and related fields
- Research Institution
  Kyoto University
Scalable Automated Program Verification for Concurrent and Parallel ProgramsPrincipal Investigator
- Principal Investigator
  
  関山太朗
- Project Period (FY)
  2024 – 2027
- Research Category
  
  Grant-in-Aid for Scientific Research (A)
- Review Section
  
  Medium-sized Section 60:Information science, computer engineering, and related fields
- Research Institution
  National Institute of Informatics
Type systems for verification of temporal and state-dependent properties in the presence of various computational effectsPrincipal Investigator
- Principal Investigator
  
  関山太朗
- Project Period (FY)
  2022 – 2024
- Research Category
  
  Grant-in-Aid for Early-Career Scientists
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  National Institute of Informatics
機械学習技術による高速な演繹的推論エンジンの開発
- Principal Investigator
  
  塚田武志
- Project Period (FY)
  2022 – 2026
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  Chiba University
Program Verification Techniques for the AI Era
- Principal Investigator
  
  小林直樹
- Project Period (FY)
  2020 – 2024
- Research Category
  
  Grant-in-Aid for Scientific Research (S)
- Review Section
  
  Broad Section J
- Research Institution
  The University of Tokyo
Research on software contracts for highly interoperable software modules
- Principal Investigator
  
  五十嵐淳
- Project Period (FY)
  2020 – 2024
- Research Category
  
  Grant-in-Aid for Scientific Research (A)
- Review Section
  
  Medium-sized Section 60:Information science, computer engineering, and related fields
- Research Institution
  Kyoto University
Automated Theorem Proving with Machine Learning for Automating Mathematics
- Principal Investigator
  
  Suenaga Kohei
- Project Period (FY)
  2019 – 2021
- Research Category
  
  Grant-in-Aid for Challenging Research (Exploratory)
- Review Section
  
  Medium-sized Section 60:Information science, computer engineering, and related fields
- Research Institution
  Kyoto University
Metatheory for gradual typing integrating dynamic and static typingPrincipal Investigator
- Principal Investigator
  
  Sekiyama Taro
- Project Period (FY)
  2019 – 2023
- Research Category
  
  Grant-in-Aid for Early-Career Scientists
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  National Institute of Informatics

All 2024 2023 2022 2021 2020 2019

All Journal Article Presentation

[Journal Article] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024
- Author(s)
  Kawamata Fuga, Unno Hiroshi, Sekiyama Taro, Terauchi Tachio
- Journal Title
  
  Proceedings of the ACM on Programming Languages (POPL)
  
  Volume: 8 Issue: POPL Pages: 115-147
- DOI
  10.1145/3633280
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H00582, KAKENHI-PROJECT-23K24820, KAKENHI-PROJECT-23K24826
[Journal Article] Space-Efficient Polymorphic Gradual Typing, Mostly Parametric2024
- Author(s)
  Atsushi Igarashi, Shota Ozaki, Taro Sekiyama, Yudai Tanabe
- Journal Title
  
  Proceedings of the ACM on Programming Languages (PLDI)
  
  Volume: - Issue: PLDI Pages: 1585-1608
- DOI
  10.1145/3656441
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H00582
[Journal Article] Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations2023
- Author(s)
  Sekiyama Taro、Unno Hiroshi
- Journal Title
  
  Proceedings of the ACM on Programming Languages
  
  Volume: 7 Issue: POPL Pages: 2079-2110
- DOI
  10.1145/3571264
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-22K17875, KAKENHI-PROJECT-20H00582, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
[Journal Article] 暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法2022
- Author(s)
  梅木孝輔、関山太朗、五十嵐淳
- Journal Title
  
  日本ソフトウェア科学会第39回大会論文集
  
  Volume: -
- Open Access
- Data Source
  KAKENHI-PROJECT-19K20247
[Journal Article] 暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法2022
- Author(s)
  梅木孝輔, 関山太朗, 五十嵐淳
- Journal Title
  
  日本ソフトウェア科学会第39回大会論文集
  
  Volume: ー
- Open Access
- Data Source
  KAKENHI-PROJECT-20H00582
[Journal Article] CPS transformation with affine types for call-by-value implicit polymorphism2021
- Author(s)
  Sekiyama Taro、Tsukada Takeshi
- Journal Title
  
  Proceedings of the ACM on Programming Languages (ICFP)
  
  Volume: 5 Issue: ICFP Pages: 1-30
- DOI
  10.1145/3473600
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-20H00582
[Journal Article] Toward Neural-Network-Guided Program Synthesis and Verification2021
- Author(s)
  Kobayashi Naoki、Sekiyama Taro、Sato Issei、Unno Hiroshi
- Journal Title
  
  Lecture Notes in Computer Science (SAS)
  
  Volume: 12913 Pages: 236-260
- DOI
  10.1007/978-3-030-88806-0_12
- ISBN
  9783030888053, 9783030888060
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
[Journal Article] Is Space-Efficient Polymorphic Gradual Typing Possible?2021
- Author(s)
  Shota Ozaki, Taro Sekiyama, Atsushi Igarashi
- Journal Title
  
  Informal Proceedings of Scheme and Functional Programming Workshop
  
  Volume: ー
- Open Access
- Data Source
  KAKENHI-PROJECT-20H00582
[Journal Article] Signature restriction for polymorphic algebraic effects2020
- Author(s)
  Sekiyama Taro、Tsukada Takeshi、Igarashi Atsushi
- Journal Title
  
  Proceedings of the ACM on Programming Languages (ICFP)
  
  Volume: 4 Issue: ICFP Pages: 1-30
- DOI
  10.1145/3408999
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-19K20247
[Journal Article] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020
- Author(s)
  Takamasa Okudono, Masaki Waga, Taro Sekiyama, Ichiro Hasuo
- Journal Title
  
  Proceedings of AAAI Conference on Artificial Intelligence (AAAI)
  
  Volume: 34 Issue: 04 Pages: 5306-5314
- DOI
  10.1609/aaai.v34i04.5977
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-15KT0012, KAKENHI-PROJECT-18J22498
[Journal Article] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020
- Author(s)
  Takamasa Okudono, Masaki Waga, Taro Sekiyama, and Ichiro Hasuo
- Journal Title
  
  Proceedings of AAAI'20
  
  Volume: －
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-19K22842
[Presentation] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024
- Author(s)
  Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
- Organizer
  ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] 限定継続のための高階プログラム論理2023
- Author(s)
  佐藤惇、関山太朗、五十嵐淳
- Organizer
  第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）
- Data Source
  KAKENHI-PROJECT-22K17875
[Presentation] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2023
- Author(s)
  Taro Sekiyama
- Organizer
  Shonan Meeting (No. 203)
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] 代数的エフェクトとハンドラのためのエフェクトシステムの抽象化2023
- Author(s)
  吉岡拓真, 関山太朗, 五十嵐淳
- Organizer
  第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations2023
- Author(s)
  Sekiyama Taro, Unno Hiroshi
- Organizer
  ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-22K17875
[Presentation] Answer-Refinement Modification: A refinement type system for algebraic effect handlers2023
- Author(s)
  Taro Sekiyama
- Organizer
  Shonan Meeting No. 203 (Effect Handlers and General-Purpose Languages)
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] 限定継続のための高階プログラム論理2023
- Author(s)
  佐藤惇, 関山太朗, 五十嵐淳
- Organizer
  第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] 代数的エフェクトハンドラのための篩型システム2023
- Author(s)
  川俣楓河、海野広志、関山太朗、寺内多智弘
- Organizer
  第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）
- Data Source
  KAKENHI-PROJECT-22K17875
[Presentation] 代数的エフェクトハンドラのための篩型システム2023
- Author(s)
  川俣楓河, 海野広志, 関山太朗, 寺内多智弘
- Organizer
  第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] 代数的エフェクトとハンドラのためのエフェクトシステムの抽象化2023
- Author(s)
  吉岡拓真、関山太朗、五十嵐淳
- Organizer
  第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）
- Data Source
  KAKENHI-PROJECT-22K17875
[Presentation] Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations2023
- Author(s)
  Taro Sekiyama, Hiroshi Unno
- Organizer
  ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] 分岐付き確率的プログラミング言語の実現に向けて2022
- Author(s)
  兼光琢真, 関山太朗
- Organizer
  第24回プログラミングおよびプログラミング言語ワークショップ（PPL 2022）
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] 計算効果入門 ― プログラミングから理論まで ―2022
- Author(s)
  関山太朗，勝股審也、叢悠悠
- Organizer
  PPLサマースクール2022
- Invited
- Data Source
  KAKENHI-PROJECT-22K17875
[Presentation] 暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法2022
- Author(s)
  梅木孝輔、関山太朗、五十嵐淳
- Organizer
  日本ソフトウェア科学会第39回大会
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] 計算効果入門 ― プログラミングから理論まで ―2022
- Author(s)
  関山太朗、勝股審也、叢悠悠
- Organizer
  PPLサマースクール2022
- Invited
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] 機械学習によるループ不変条件の発見2021
- Author(s)
  関山太朗
- Organizer
  第24回情報論的学習理論ワークショップ（企画セッション1：ソフトウェア検証と機械学習）
- Invited
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] Is Space-Efficient Polymorphic Gradual Typing Possible?2021
- Author(s)
  Shota Ozaki, Taro Sekiyama, Atsushi Igarashi
- Organizer
  Scheme and Functional Programming Workshop
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] CPS transformation with affine types for call-by-value implicit polymorphism2021
- Author(s)
  Sekiyama Taro
- Organizer
  International Conference on Functional Programming (ICFP)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] レコードとハッシュテーブルの暗黙な相互運用を可能にする型推論とコンパイル手法2021
- Author(s)
  梅木孝輔, 関山太朗, 五十嵐淳
- Organizer
  第23回プログラミングおよびプログラミング言語ワークショップ(PPL2021)
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] Signature Restriction for Polymorphic Algebraic Effects ICFP 20202021
- Author(s)
  Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
- Organizer
  第23回プログラミングおよびプログラミング言語ワークショップ (PPL2021)
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] レコードとハッシュテーブルの暗黙な相互運用を可能にする型推論とコンパイル手法2021
- Author(s)
  梅木孝輔, 関山太朗, 五十嵐淳
- Organizer
  第23回プログラミングおよびプログラミング言語ワークショップ (PPL2021)
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] CPS transformation with affine types for call-by-value implicit polymorphism2021
- Author(s)
  Taro Sekiyama, Takeshi Tsukada
- Organizer
  ACM SIGPLAN International Conference on Functional Programming (ICFP)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-20H00582
[Presentation] CPS Transformation with Affine Types for Implicit Polymorphism2021
- Author(s)
  Sekiyama Taro
- Organizer
  Dagstuhl Seminar 20312, Scalable Handling of Effects
- Invited / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces2020
- Author(s)
  Takamasa Okudono, Masaki Waga, Taro Sekiyama, Ichiro Hasuo
- Organizer
  AAAI Conference on Artificial Intelligence (AAAI)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] Signature restriction for polymorphic algebraic effects2020
- Author(s)
  Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
- Organizer
  The 25th ACM SIGPLAN International Conference on Functional Programming (ICFP)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] Gradual Typing for Extensibility by Rows2020
- Author(s)
  Taro Sekiyama, Atsushi Igarashi
- Organizer
  ACM SIGPLAN Workshop on Gradual Typing (WGT)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-19K20247
[Presentation] Weighted Automata Extraction from Recurrent Neural Networks via Regression2019
- Author(s)
  関山太朗
- Organizer
  第22回情報論的学習理論ワークショップ
- Invited
- Data Source
  KAKENHI-PROJECT-19K20247

1. Suenaga Kohei (70633692)

# of Collaborated Projects: 4 results

# of Collaborated Products: 0 results
2. 塚田武志 (50758951)

# of Collaborated Projects: 3 results

# of Collaborated Products: 0 results
3. 五十嵐淳 (40323456)

# of Collaborated Projects: 3 results

# of Collaborated Products: 6 results
4. 海野広志 (80569575)

# of Collaborated Projects: 3 results

# of Collaborated Products: 0 results
5. 池渕未来 (70961796)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
6. 小林直樹 (00262155)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
7. 吉仲亮 (80466424)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
8. 佐藤一誠 (90610155)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
9. 佐藤亮介 (10804677)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
10. 田邉裕大 (30985198)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
11. 松下祐介 (41003875)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
12. 和賀正樹 (00899007)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results

Sekiyama Taro 関山 太朗

Research Projects

Research Products

Co-Researchers

AIを含むソフトウェアのための形式検証手法

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Scalable Automated Program Verification for Concurrent and Parallel ProgramsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Type systems for verification of temporal and state-dependent properties in the presence of various computational effectsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

機械学習技術による高速な演繹的推論エンジンの開発

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Program Verification Techniques for the AI Era

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Research on software contracts for highly interoperable software modules

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Automated Theorem Proving with Machine Learning for Automating Mathematics

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Metatheory for gradual typing integrating dynamic and static typingPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

[Journal Article] Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers2024

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Space-Efficient Polymorphic Gradual Typing, Mostly Parametric2024

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations2023

Author(s)

Journal Title

DOI

Data Source

[Journal Article] 暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法2022

Author(s)

Journal Title

Data Source

[Journal Article] 暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法2022

Author(s)

Journal Title

Data Source

[Journal Article] CPS transformation with affine types for call-by-value implicit polymorphism2021

Author(s)

Journal Title

DOI

Data Source

Sekiyama Taro 関山太朗