• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

先進的型理論に基づく多段階計算体系の設計と実装

研究課題

研究課題/領域番号 18H03218
研究種目

基盤研究(B)

配分区分補助金
応募区分一般
審査区分 小区分60050:ソフトウェア関連
研究機関筑波大学

研究代表者

亀山 幸義  筑波大学, システム情報系, 教授 (10195000)

研究分担者 浅井 健一  お茶の水女子大学, 基幹研究院, 教授 (10262156)
Kiselyov Oleg  東北大学, 情報科学研究科, 助教 (50754602)
研究期間 (年度) 2018-04-01 – 2022-03-31
研究課題ステータス 完了 (2022年度)
配分額 *注記
12,740千円 (直接経費: 9,800千円、間接経費: 2,940千円)
2021年度: 2,860千円 (直接経費: 2,200千円、間接経費: 660千円)
2020年度: 3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2019年度: 2,600千円 (直接経費: 2,000千円、間接経費: 600千円)
2018年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
キーワードプログラム生成 / 多段階計算 / 型システム / 型安全性 / モジュール / 計算エフェクト / 異種プログラム生成 / プログラムの信頼性 / 段階的計算 / 先進的型システム / コントロールオペレータ / プログラム解析 / 高性能計算 / 依存型 / 一般化代数データ型 / 静的安全性 / モジュール抽象 / ヘテロジニアスプログラム生成 / 統合言語クエリ / 多相型 / スクープ安全性 / 安全性
研究成果の概要

多段階計算法(マルチステージプログラミング)は、プログラムを用いてプログラムを生成する手法のことであり、パラメータや計算環境に特化した高性能プログラムを得られるものである。この手法は、すでに多数の分野で利用されているが、利用されている先進的な機能の中には型システムなどの保証がないものが多い。
本研究は、安全で信頼できるプログラム生成とするため、モジュールを型安全に生成する仕組み、ジャンプなどの計算エフェクト(副作用)を持つプログラムの型システム、異種プログラム生成(高レベルプログラムを用いた低レベルプログラムの生成)という3点について研究を行い、それぞれ従来の限界を突破する成果をあげた。

研究成果の学術的意義や社会的意義

本研究の学術的な意義は、従来の多段階計算の限界を突破して、現実に必要とされる広い範囲の言語機構に対する「型安全なプログラム生成」を保証するために必要な型理論的基礎を構築したことである。具体的には、モジュールのコードの生成、代数的効果、異種プログラム生成などに対応し、かつ、型安全性を保証された多段階計算体系は、オリジナリティが非常に高い研究であると考えている。
社会的意義については、MetaOCaml言語における異種プログラム生成機能の実装や、高性能ソフトウェアラジオの実装などがあげられる。

報告書

(5件)
  • 2022 研究成果報告書 ( PDF )
  • 2021 実績報告書
  • 2020 実績報告書
  • 2019 実績報告書
  • 2018 実績報告書
  • 研究成果

    (53件)

すべて 2022 2021 2020 2019 2018 その他

すべて 国際共同研究 (1件) 雑誌論文 (22件) (うち国際共著 5件、 査読あり 19件、 オープンアクセス 2件) 学会発表 (26件) (うち国際学会 16件) 図書 (1件) 備考 (3件)

  • [国際共同研究] Cambridge Univesrity(英国)

    • 関連する報告書
      2018 実績報告書
  • [雑誌論文] 4種類の限定継続演算子のための型システム2022

    • 著者名/発表者名
      石尾 千晶、浅井 健一
    • 雑誌名

      第24回プログラミングおよびプログラミング言語ワークショップ論文集

      巻: -

    • 関連する報告書
      2021 実績報告書
    • 査読あり
  • [雑誌論文] 代数的エフェクトとハンドラのための CPS インタプリタと型システム2022

    • 著者名/発表者名
      藤井 舞花、浅井 健一
    • 雑誌名

      第24回プログラミングおよびプログラミング言語ワークショップ論文集

      巻: -

    • 関連する報告書
      2021 実績報告書
    • 査読あり
  • [雑誌論文] FFT Program Generation for Ring LWE-Based Cryptography2021

    • 著者名/発表者名
      Masahiro Masuda and Yukiyoshi Kameyama
    • 雑誌名

      Lecture Notes in Computer Science

      巻: 12835 ページ: 151-171

    • DOI

      10.1007/978-3-030-85987-9_9

    • ISBN
      9783030859862, 9783030859879
    • 関連する報告書
      2021 実績報告書
    • 査読あり
  • [雑誌論文] Type-safe generation of modules in applicative and generative styles2021

    • 著者名/発表者名
      Yuhi Sato and Yukiyoshi Kameyama
    • 雑誌名

      Proceedings of 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE 2021)

      巻: - ページ: 184-196

    • DOI

      10.1145/3486609.3487209

    • 関連する報告書
      2021 実績報告書
    • 査読あり
  • [雑誌論文] A Functional Abstraction of Typed Invocation Contexts2021

    • 著者名/発表者名
      Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai
    • 雑誌名

      6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

      巻: -

    • 関連する報告書
      2021 実績報告書
    • 査読あり
  • [雑誌論文] Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators2021

    • 著者名/発表者名
      Maika Fujii and Kenichi Asai
    • 雑誌名

      6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

      巻: -

    • 関連する報告書
      2021 実績報告書
    • 査読あり
  • [雑誌論文] Not by equations alone: Reasoning with extensible effects2021

    • 著者名/発表者名
      KISELYOV OLEG、MU SHIN-CHENG、SABRY AMR
    • 雑誌名

      Journal of Functional Programming

      巻: 31

    • DOI

      10.1017/s0956796820000271

    • 関連する報告書
      2020 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] control/prompt の仮想機械導出2021

    • 著者名/発表者名
      藤井 舞花、浅井 健一
    • 雑誌名

      第23回プログラミングおよびプログラミング言語ワークショップ論文集

      巻: ー ページ: 1-19

    • 関連する報告書
      2020 実績報告書
    • 査読あり
  • [雑誌論文] One-Shot Algebraic Effects as Coroutines2020

    • 著者名/発表者名
      Kawahara Satoru、Kameyama Yukiyoshi
    • 雑誌名

      Lecture Notes in Computer Science

      巻: 12222 ページ: 159-179

    • DOI

      10.1007/978-3-030-57761-2_8

    • ISBN
      9783030577605, 9783030577612
    • 関連する報告書
      2020 実績報告書
    • 査読あり
  • [雑誌論文] Reorganizing queries with grouping2020

    • 著者名/発表者名
      Okura Rui、Kameyama Yukiyoshi
    • 雑誌名

      GPCE '20: Proceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences

      巻: ー ページ: 50-62

    • DOI

      10.1145/3425898.3426960

    • 関連する報告書
      2020 実績報告書
    • 査読あり
  • [雑誌論文] Language-Integrated Query with Nested Data Structures and Grouping2020

    • 著者名/発表者名
      Okura Rui、Kameyama Yukiyoshi
    • 雑誌名

      Lecture Notes in Computer Science

      巻: 12073 ページ: 139-158

    • DOI

      10.1007/978-3-030-59025-3_9

    • ISBN
      9783030590246, 9783030590253
    • 関連する報告書
      2020 実績報告書
    • 査読あり
  • [雑誌論文] Session Types Without Sophistry2020

    • 著者名/発表者名
      Kiselyov Oleg、Imai Keigo
    • 雑誌名

      Lecture Notes in Computer Science

      巻: 12073 ページ: 66-87

    • DOI

      10.1007/978-3-030-59025-3_5

    • ISBN
      9783030590246, 9783030590253
    • 関連する報告書
      2020 実績報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] 型付きDSLに対するプログラム変換の型安全なフレームワーク2020

    • 著者名/発表者名
      高木 尚、亀山 幸義
    • 雑誌名

      日本ソフトウェア科学会第37回大会講演論文集

      巻: ー ページ: 1-10

    • 関連する報告書
      2020 実績報告書
  • [雑誌論文] Module Generation without Regret2020

    • 著者名/発表者名
      uhi Sato, Yukiyoshi Kameyama, Takahisa Watanabe
    • 雑誌名

      Proc. of ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

      巻: - ページ: 1-13

    • DOI

      10.1145/3372884.3373160

    • 関連する報告書
      2019 実績報告書
    • 査読あり
  • [雑誌論文] Verifying Selective CPS Transformation for Shift and Reset2020

    • 著者名/発表者名
      Chiaki Ishio, Kenichi Asai
    • 雑誌名

      Lecture Notes in Computer Science

      巻: 12053 ページ: 38-57

    • DOI

      10.1007/978-3-030-47147-7_3

    • ISBN
      9783030471460, 9783030471477
    • 関連する報告書
      2019 実績報告書
    • 査読あり
  • [雑誌論文] 限定継続命令をもつ依存型付き言語の設計2019

    • 著者名/発表者名
      叢 悠悠、浅井 健一
    • 雑誌名

      コンピュータ ソフトウェア

      巻: 36 号: 2 ページ: 2_47-2_60

    • DOI

      10.11309/jssst.36.2_47

    • NAID

      130007667001

    • ISSN
      0289-6540
    • 年月日
      2019-04-26
    • 関連する報告書
      2019 実績報告書
    • 査読あり
  • [雑誌論文] Extracting a Call-by-Name Partial Evaluator from a Proof of Termination2019

    • 著者名/発表者名
      Kenichi Asai
    • 雑誌名

      ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '19)

      巻: - ページ: 61-67

    • DOI

      10.1145/3294032.3294084

    • 関連する報告書
      2018 実績報告書
    • 査読あり
  • [雑誌論文] Generating Mutually Recursive Definitions2019

    • 著者名/発表者名
      Jeremy Yallop, Oleg Kiselyov
    • 雑誌名

      Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

      巻: - ページ: 75-81

    • DOI

      10.1145/3294032.3294078

    • 関連する報告書
      2018 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] Meta-Programming for Statistical Machine Learning2018

    • 著者名/発表者名
      Oleg Kiselyov, Tiark Rompf, Jennifer Neville, Yukiyoshi Kameyama
    • 雑誌名

      NII Shonan Seminar Report,

      巻: No. 2018-7

    • 関連する報告書
      2018 実績報告書
    • 国際共著
  • [雑誌論文] Handling Delimited Continuations with Dependent Types2018

    • 著者名/発表者名
      Youyou Cong, and Kenichi Asai
    • 雑誌名

      Proceedings of the ACM on Programming Languages

      巻: Vol. 2, Issue ICFP 号: ICFP ページ: 31-31

    • DOI

      10.1145/3236764

    • 関連する報告書
      2018 実績報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Certifying CPS Transformation of Let-polymorphic Calculus Using PHOAS2018

    • 著者名/発表者名
      Urara Yamada, and Kenichi Asai
    • 雑誌名

      16th Asian Symposium on Programming Languages and Systems (APLAS 2018),LNCS 11275

      巻: - ページ: 375-393

    • DOI

      10.1007/978-3-030-02768-1_20

    • ISBN
      9783030027674, 9783030027681
    • 関連する報告書
      2018 実績報告書
    • 査読あり
  • [雑誌論文] Functional Stream Libraries and Fusion: What's Next?2018

    • 著者名/発表者名
      Aggelos Biboudis (EPFL, Switzerland), Oleg Kiselyov, Martin Odersky (EPFL, Switzerland)
    • 雑誌名

      NII Shonan Seminar Report

      巻: No.2018-14

    • 関連する報告書
      2018 実績報告書
    • 国際共著
  • [学会発表] let (rec) insertion without Effects, Lights or Magic2022

    • 著者名/発表者名
      Oleg Kiselyov and Jeremy Yallop
    • 学会等名
      ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2022)
    • 関連する報告書
      2021 実績報告書
    • 国際学会
  • [学会発表] FFT Program Generation for Ring LWE-Based Cryptography2021

    • 著者名/発表者名
      Masahiro Masuda and Yukiyoshi Kameyama
    • 学会等名
      16th International Workshop on Security (IWSEC 2021)
    • 関連する報告書
      2021 実績報告書
    • 国際学会
  • [学会発表] Type-safe generation of modules in applicative and generative styles2021

    • 著者名/発表者名
      Yuhi Sato and Yukiyoshi Kameyama
    • 学会等名
      20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE 2021)
    • 関連する報告書
      2021 実績報告書
    • 国際学会
  • [学会発表] A Functional Abstraction of Typed Invocation Contexts2021

    • 著者名/発表者名
      Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai
    • 学会等名
      6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
    • 関連する報告書
      2021 実績報告書
    • 国際学会
  • [学会発表] Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators2021

    • 著者名/発表者名
      Maika Fujii and Kenichi Asai
    • 学会等名
      6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
    • 関連する報告書
      2021 実績報告書
    • 国際学会
  • [学会発表] control/prompt の仮想機械導出2021

    • 著者名/発表者名
      藤井 舞花, 浅井 健一
    • 学会等名
      第23回プログラミングおよびプログラミング言語ワークショップ
    • 関連する報告書
      2020 実績報告書
  • [学会発表] 配列言語の長所を分かりやすく味わう: OCaml上の埋め込み配列言語2021

    • 著者名/発表者名
      庄司諭 Oleg Kiselyov
    • 学会等名
      第23回プログラミングおよびプログラミング言語ワークショップ
    • 関連する報告書
      2020 実績報告書
  • [学会発表] A Functional Abstraction of Typed Trails2021

    • 著者名/発表者名
      Asai Kenichi, Cong Youyou, Ishio Chiaki
    • 学会等名
      ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '21)
    • 関連する報告書
      2020 実績報告書
    • 国際学会
  • [学会発表] Language-Integrated Query with Nested Data Structures and Grouping2020

    • 著者名/発表者名
      Okura Rui, Kameyama Yukiyoshi
    • 学会等名
      International Symposium on Functional and Logic Programming (FLOPS 2020)
    • 関連する報告書
      2020 実績報告書
    • 国際学会
  • [学会発表] Reorganizing queries with grouping2020

    • 著者名/発表者名
      Okura Rui, Kameyama Yukiyoshi
    • 学会等名
      Tthe 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE '20)
    • 関連する報告書
      2020 実績報告書
    • 国際学会
  • [学会発表] 型付きDSLに対するプログラム変換の型安全なフレームワーク2020

    • 著者名/発表者名
      高木 尚, 亀山 幸義
    • 学会等名
      日本ソフトウェア科学会第37回大会
    • 関連する報告書
      2020 実績報告書
  • [学会発表] Session Types without Sophistry2020

    • 著者名/発表者名
      Keigo Imai, Oleg Kiselyov
    • 学会等名
      nternational Symposium on Functional and Logic Programming (FLOPS 2020)
    • 関連する報告書
      2020 実績報告書
    • 国際学会
  • [学会発表] より清浄なStream Fusion2020

    • 著者名/発表者名
      小林 友明, Oleg Kiselyov
    • 学会等名
      日本ソフトウェア科学会第37回大会
    • 関連する報告書
      2020 実績報告書
  • [学会発表] Module Generation without Regret2020

    • 著者名/発表者名
      Yuhi Sato, Yukiyoshi Kameyama, Takahisa Watanabe
    • 学会等名
      2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] One-shot Algebraic Effects as Coroutines2020

    • 著者名/発表者名
      Satoru Kawahara, Yukiyoshi Kameyama
    • 学会等名
      21st International Symposium on Trends in Functional Programming
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Agda の Reflection API を用いた自動証明に向けて2020

    • 著者名/発表者名
      石尾 千晶、山本 充子、浅井 健一
    • 学会等名
      第22回プログラミングおよびプログラミング言語ワークショップ
    • 関連する報告書
      2019 実績報告書
  • [学会発表] algebraic effects を含むプログラムのステップ実行2020

    • 著者名/発表者名
      古川 つきの、浅井 健一
    • 学会等名
      第22回プログラミングおよびプログラミング言語ワークショップ
    • 関連する報告書
      2019 実績報告書
  • [学会発表] let (rec) insertion without effects, lights or magic2019

    • 著者名/発表者名
      Oleg Kiselyov, Jeremy Yallop
    • 学会等名
      ML Family Workshop
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Session Types without Sophistry: Practical embedding of DSLs with sophisticated type systems2019

    • 著者名/発表者名
      Oleg Kiselyov
    • 学会等名
      IFIP WG2.11 20th Meeting
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Language-Integrated Query with Nested Data Structures and Grouping2019

    • 著者名/発表者名
      Yukiyoshi Kameyama
    • 学会等名
      IFIP WG2.11 20th Meeting
    • 関連する報告書
      2019 実績報告書
    • 国際学会
  • [学会発表] Polymorphic Staged Calculus with Cross-Stage Persistence and Side Effects2019

    • 著者名/発表者名
      菊地 綾音,亀山 幸義
    • 学会等名
      情報処理学会第122回プログラミング研究発表会
    • 関連する報告書
      2018 実績報告書
  • [学会発表] 動的変数をもつ依存型付きラムダ計算2019

    • 著者名/発表者名
      叢 悠悠、浅井 健一
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ論文集
    • 関連する報告書
      2018 実績報告書
  • [学会発表] shift/reset のための selective CPS 変換の正当性 の証明2019

    • 著者名/発表者名
      石尾 千晶、浅井 健一
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ論文集
    • 関連する報告書
      2018 実績報告書
  • [学会発表] セッション型、簡潔に2019

    • 著者名/発表者名
      オレッグ キセリョーヴ 今井 敬吾
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ (poster)
    • 関連する報告書
      2018 実績報告書
  • [学会発表] A Lightweight Approach to Module Generation2018

    • 著者名/発表者名
      Yukiyoshi Kameyama
    • 学会等名
      IFIP Working Group 2.11, 18th meeting (Kyoto, Japan)
    • 関連する報告書
      2018 実績報告書
    • 国際学会
  • [学会発表] Session types without sophistry2018

    • 著者名/発表者名
      Oleg Kiselyov
    • 学会等名
      IFIP Working Group 2.11, 18th meeting (Kyoto, Japan)
    • 関連する報告書
      2018 実績報告書
    • 国際学会
  • [図書] NII Shonan Meeting report No. 1462019

    • 著者名/発表者名
      Sam Lindley, Nicolas Wu, Oleg Kiselyov, Gordon Plotkin
    • 総ページ数
      11
    • 出版者
      Programming and Reasoning with Algebraic Effects and Effect Handlers
    • 関連する報告書
      2019 実績報告書
  • [備考] メタプログラミング研究集会 (Workshop on Metaprogramming)

    • URL

      https://www.cs.tsukuba.ac.jp/~kam/meta2022/

    • 関連する報告書
      2021 実績報告書
  • [備考] Yukiyoshi Kameyama's Publication

    • URL

      http://www.cs.tsukuba.ac.jp/~kam/publication.html

    • 関連する報告書
      2020 実績報告書
  • [備考]

    • URL

      http://www.cs.tsukuba.ac.jp/~kam/publication.html

    • 関連する報告書
      2019 実績報告書

URL: 

公開日: 2018-04-23   更新日: 2024-01-30  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi