• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Staged Computing based on Advanced Type Systems

Research Project

Project/Area Number 18H03218
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Review Section Basic Section 60050:Software-related
Research InstitutionUniversity of Tsukuba

Principal Investigator

Kameyama Yukiyoshi  筑波大学, システム情報系, 教授 (10195000)

Co-Investigator(Kenkyū-buntansha) 浅井 健一  お茶の水女子大学, 基幹研究院, 教授 (10262156)
Kiselyov Oleg  東北大学, 情報科学研究科, 助教 (50754602)
Project Period (FY) 2018-04-01 – 2022-03-31
Project Status Completed (Fiscal Year 2022)
Budget Amount *help
¥12,740,000 (Direct Cost: ¥9,800,000、Indirect Cost: ¥2,940,000)
Fiscal Year 2021: ¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2020: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2019: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
Fiscal Year 2018: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Keywordsプログラム生成 / 多段階計算 / 型システム / 型安全性 / モジュール / 計算エフェクト / 異種プログラム生成 / プログラムの信頼性 / 段階的計算 / 先進的型システム / コントロールオペレータ / プログラム解析 / 高性能計算 / 依存型 / 一般化代数データ型 / 静的安全性 / モジュール抽象 / ヘテロジニアスプログラム生成 / 統合言語クエリ / 多相型 / スクープ安全性 / 安全性
Outline of Final Research Achievements

Multi-stage programming is a means to generate programs by programs, by specializing a program by parameters or computation environments. Although it has been used in various application fields, there are many advanced features used in these applications which are not guaranteed to be safe or reliable. This research project aims to ensure the safety and reliability of generated programs. We have obtained a calculus for type-safe generation of modules, type systems for control operators that are proven sound, and a rigid formulation of heterogeneous program generation.

Academic Significance and Societal Importance of the Research Achievements

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

Report

(5 results)
  • 2022 Final Research Report ( PDF )
  • 2021 Annual Research Report
  • 2020 Annual Research Report
  • 2019 Annual Research Report
  • 2018 Annual Research Report
  • Research Products

    (53 results)

All 2022 2021 2020 2019 2018 Other

All Int'l Joint Research (1 results) Journal Article (22 results) (of which Int'l Joint Research: 5 results,  Peer Reviewed: 19 results,  Open Access: 2 results) Presentation (26 results) (of which Int'l Joint Research: 16 results) Book (1 results) Remarks (3 results)

  • [Int'l Joint Research] Cambridge Univesrity(英国)

    • Related Report
      2018 Annual Research Report
  • [Journal Article] 4種類の限定継続演算子のための型システム2022

    • Author(s)
      石尾 千晶、浅井 健一
    • Journal Title

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

      Volume: -

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 代数的エフェクトとハンドラのための CPS インタプリタと型システム2022

    • Author(s)
      藤井 舞花、浅井 健一
    • Journal Title

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

      Volume: -

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] FFT Program Generation for Ring LWE-Based Cryptography2021

    • Author(s)
      Masahiro Masuda and Yukiyoshi Kameyama
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 12835 Pages: 151-171

    • DOI

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

    • ISBN
      9783030859862, 9783030859879
    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Type-safe generation of modules in applicative and generative styles2021

    • Author(s)
      Yuhi Sato and Yukiyoshi Kameyama
    • Journal Title

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

      Volume: - Pages: 184-196

    • DOI

      10.1145/3486609.3487209

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A Functional Abstraction of Typed Invocation Contexts2021

    • Author(s)
      Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai
    • Journal Title

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

      Volume: -

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators2021

    • Author(s)
      Maika Fujii and Kenichi Asai
    • Journal Title

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

      Volume: -

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Not by equations alone: Reasoning with extensible effects2021

    • Author(s)
      KISELYOV OLEG、MU SHIN-CHENG、SABRY AMR
    • Journal Title

      Journal of Functional Programming

      Volume: 31

    • DOI

      10.1017/s0956796820000271

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] control/prompt の仮想機械導出2021

    • Author(s)
      藤井 舞花、浅井 健一
    • Journal Title

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

      Volume: ー Pages: 1-19

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] One-Shot Algebraic Effects as Coroutines2020

    • Author(s)
      Kawahara Satoru、Kameyama Yukiyoshi
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 12222 Pages: 159-179

    • DOI

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

    • ISBN
      9783030577605, 9783030577612
    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Reorganizing queries with grouping2020

    • Author(s)
      Okura Rui、Kameyama Yukiyoshi
    • Journal Title

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

      Volume: ー Pages: 50-62

    • DOI

      10.1145/3425898.3426960

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Language-Integrated Query with Nested Data Structures and Grouping2020

    • Author(s)
      Okura Rui、Kameyama Yukiyoshi
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 12073 Pages: 139-158

    • DOI

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

    • ISBN
      9783030590246, 9783030590253
    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Session Types Without Sophistry2020

    • Author(s)
      Kiselyov Oleg、Imai Keigo
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 12073 Pages: 66-87

    • DOI

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

    • ISBN
      9783030590246, 9783030590253
    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] 型付きDSLに対するプログラム変換の型安全なフレームワーク2020

    • Author(s)
      高木 尚、亀山 幸義
    • Journal Title

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

      Volume: ー Pages: 1-10

    • Related Report
      2020 Annual Research Report
  • [Journal Article] Module Generation without Regret2020

    • Author(s)
      uhi Sato, Yukiyoshi Kameyama, Takahisa Watanabe
    • Journal Title

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

      Volume: - Pages: 1-13

    • DOI

      10.1145/3372884.3373160

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Verifying Selective CPS Transformation for Shift and Reset2020

    • Author(s)
      Chiaki Ishio, Kenichi Asai
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 12053 Pages: 38-57

    • DOI

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

    • ISBN
      9783030471460, 9783030471477
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A Dependently Typed Language with Delimited Control Operators.2019

    • Author(s)
      叢 悠悠、浅井 健一
    • Journal Title

      Computer Software

      Volume: 36 Issue: 2 Pages: 2_47-2_60

    • DOI

      10.11309/jssst.36.2_47

    • NAID

      130007667001

    • ISSN
      0289-6540
    • Year and Date
      2019-04-26
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Extracting a Call-by-Name Partial Evaluator from a Proof of Termination2019

    • Author(s)
      Kenichi Asai
    • Journal Title

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

      Volume: - Pages: 61-67

    • DOI

      10.1145/3294032.3294084

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Generating Mutually Recursive Definitions2019

    • Author(s)
      Jeremy Yallop, Oleg Kiselyov
    • Journal Title

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

      Volume: - Pages: 75-81

    • DOI

      10.1145/3294032.3294078

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Meta-Programming for Statistical Machine Learning2018

    • Author(s)
      Oleg Kiselyov, Tiark Rompf, Jennifer Neville, Yukiyoshi Kameyama
    • Journal Title

      NII Shonan Seminar Report,

      Volume: No. 2018-7

    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Journal Article] Handling Delimited Continuations with Dependent Types2018

    • Author(s)
      Youyou Cong, and Kenichi Asai
    • Journal Title

      Proceedings of the ACM on Programming Languages

      Volume: Vol. 2, Issue ICFP Issue: ICFP Pages: 31-31

    • DOI

      10.1145/3236764

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Certifying CPS Transformation of Let-polymorphic Calculus Using PHOAS2018

    • Author(s)
      Urara Yamada, and Kenichi Asai
    • Journal Title

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

      Volume: - Pages: 375-393

    • DOI

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

    • ISBN
      9783030027674, 9783030027681
    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Functional Stream Libraries and Fusion: What's Next?2018

    • Author(s)
      Aggelos Biboudis (EPFL, Switzerland), Oleg Kiselyov, Martin Odersky (EPFL, Switzerland)
    • Journal Title

      NII Shonan Seminar Report

      Volume: No.2018-14

    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] let (rec) insertion without Effects, Lights or Magic2022

    • Author(s)
      Oleg Kiselyov and Jeremy Yallop
    • Organizer
      ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2022)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] FFT Program Generation for Ring LWE-Based Cryptography2021

    • Author(s)
      Masahiro Masuda and Yukiyoshi Kameyama
    • Organizer
      16th International Workshop on Security (IWSEC 2021)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Type-safe generation of modules in applicative and generative styles2021

    • Author(s)
      Yuhi Sato and Yukiyoshi Kameyama
    • Organizer
      20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE 2021)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] A Functional Abstraction of Typed Invocation Contexts2021

    • Author(s)
      Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai
    • Organizer
      6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators2021

    • Author(s)
      Maika Fujii and Kenichi Asai
    • Organizer
      6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] control/prompt の仮想機械導出2021

    • Author(s)
      藤井 舞花, 浅井 健一
    • Organizer
      第23回プログラミングおよびプログラミング言語ワークショップ
    • Related Report
      2020 Annual Research Report
  • [Presentation] 配列言語の長所を分かりやすく味わう: OCaml上の埋め込み配列言語2021

    • Author(s)
      庄司諭 Oleg Kiselyov
    • Organizer
      第23回プログラミングおよびプログラミング言語ワークショップ
    • Related Report
      2020 Annual Research Report
  • [Presentation] A Functional Abstraction of Typed Trails2021

    • Author(s)
      Asai Kenichi, Cong Youyou, Ishio Chiaki
    • Organizer
      ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '21)
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Language-Integrated Query with Nested Data Structures and Grouping2020

    • Author(s)
      Okura Rui, Kameyama Yukiyoshi
    • Organizer
      International Symposium on Functional and Logic Programming (FLOPS 2020)
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Reorganizing queries with grouping2020

    • Author(s)
      Okura Rui, Kameyama Yukiyoshi
    • Organizer
      Tthe 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE '20)
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 型付きDSLに対するプログラム変換の型安全なフレームワーク2020

    • Author(s)
      高木 尚, 亀山 幸義
    • Organizer
      日本ソフトウェア科学会第37回大会
    • Related Report
      2020 Annual Research Report
  • [Presentation] Session Types without Sophistry2020

    • Author(s)
      Keigo Imai, Oleg Kiselyov
    • Organizer
      nternational Symposium on Functional and Logic Programming (FLOPS 2020)
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] より清浄なStream Fusion2020

    • Author(s)
      小林 友明, Oleg Kiselyov
    • Organizer
      日本ソフトウェア科学会第37回大会
    • Related Report
      2020 Annual Research Report
  • [Presentation] Module Generation without Regret2020

    • Author(s)
      Yuhi Sato, Yukiyoshi Kameyama, Takahisa Watanabe
    • Organizer
      2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] One-shot Algebraic Effects as Coroutines2020

    • Author(s)
      Satoru Kawahara, Yukiyoshi Kameyama
    • Organizer
      21st International Symposium on Trends in Functional Programming
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Agda の Reflection API を用いた自動証明に向けて2020

    • Author(s)
      石尾 千晶、山本 充子、浅井 健一
    • Organizer
      第22回プログラミングおよびプログラミング言語ワークショップ
    • Related Report
      2019 Annual Research Report
  • [Presentation] algebraic effects を含むプログラムのステップ実行2020

    • Author(s)
      古川 つきの、浅井 健一
    • Organizer
      第22回プログラミングおよびプログラミング言語ワークショップ
    • Related Report
      2019 Annual Research Report
  • [Presentation] let (rec) insertion without effects, lights or magic2019

    • Author(s)
      Oleg Kiselyov, Jeremy Yallop
    • Organizer
      ML Family Workshop
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Session Types without Sophistry: Practical embedding of DSLs with sophisticated type systems2019

    • Author(s)
      Oleg Kiselyov
    • Organizer
      IFIP WG2.11 20th Meeting
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Language-Integrated Query with Nested Data Structures and Grouping2019

    • Author(s)
      Yukiyoshi Kameyama
    • Organizer
      IFIP WG2.11 20th Meeting
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Polymorphic Staged Calculus with Cross-Stage Persistence and Side Effects2019

    • Author(s)
      菊地 綾音,亀山 幸義
    • Organizer
      情報処理学会第122回プログラミング研究発表会
    • Related Report
      2018 Annual Research Report
  • [Presentation] 動的変数をもつ依存型付きラムダ計算2019

    • Author(s)
      叢 悠悠、浅井 健一
    • Organizer
      第21回プログラミングおよびプログラミング言語ワークショップ論文集
    • Related Report
      2018 Annual Research Report
  • [Presentation] shift/reset のための selective CPS 変換の正当性 の証明2019

    • Author(s)
      石尾 千晶、浅井 健一
    • Organizer
      第21回プログラミングおよびプログラミング言語ワークショップ論文集
    • Related Report
      2018 Annual Research Report
  • [Presentation] セッション型、簡潔に2019

    • Author(s)
      オレッグ キセリョーヴ 今井 敬吾
    • Organizer
      第21回プログラミングおよびプログラミング言語ワークショップ (poster)
    • Related Report
      2018 Annual Research Report
  • [Presentation] A Lightweight Approach to Module Generation2018

    • Author(s)
      Yukiyoshi Kameyama
    • Organizer
      IFIP Working Group 2.11, 18th meeting (Kyoto, Japan)
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Session types without sophistry2018

    • Author(s)
      Oleg Kiselyov
    • Organizer
      IFIP Working Group 2.11, 18th meeting (Kyoto, Japan)
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Book] NII Shonan Meeting report No. 1462019

    • Author(s)
      Sam Lindley, Nicolas Wu, Oleg Kiselyov, Gordon Plotkin
    • Total Pages
      11
    • Publisher
      Programming and Reasoning with Algebraic Effects and Effect Handlers
    • Related Report
      2019 Annual Research Report
  • [Remarks] メタプログラミング研究集会 (Workshop on Metaprogramming)

    • URL

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

    • Related Report
      2021 Annual Research Report
  • [Remarks] Yukiyoshi Kameyama's Publication

    • URL

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

    • Related Report
      2020 Annual Research Report
  • [Remarks]

    • URL

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

    • Related Report
      2019 Annual Research Report

URL: 

Published: 2018-04-23   Modified: 2024-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi