Multi-Stage Programming with Dependent Types: Theory and Implementation

具有依赖类型的多阶段编程：理论与实现

• 批准号: 22H03563
• 负责人: 亀山 幸義
• 金额: $ 11.07万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2022
• 资助国家: 日本
• 起止时间: 2022-04-01 至 2026-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-22H03563/
• 关键词: プログラム生成; プログラム特化; 型システム; 依存型; 仕様記述; 段階的計算; プログラム解析・検証; 計算エフェクト; オフショアリング

研究初年度となる２０２２年度は、本研究の基盤となる段階的計算体系において、計算リソース（メモリ量など）や生成されたコードのサイズ・性能などの量を扱うプログラム生成技法とその実例について調査を行った。特に、依存型を用いない従来型の型システムにおいてこれらの量的な情報をもとに質の高いプログラムを生成したりプログラム解析・検証を行った成功例について詳細に検討を行った。そのような研究の１つとして、亀山らが開発してきたプログラム生成・解析・検証を統一して行うフレームワークについて、暗号分野の適用事例をさらに洗練させて性能向上を果たした。特に、従来は、数論的変換関数だけの実装にとどまっていたのに対し、本研究では、多項式乗算など、より大きな関数を適用対象として、高性能コードの生成とその正しさの検証を同時に達成することに成功した。上記と並行して、コード重複を回避する段階的計算において重要となる計算エフェクトについて理論・実装の両面からの研究を行い、代数的エフェクトと限定継続コントロールオペレータの関係を解明したり、限定継続コントロールオペレータに関する統一的型システムを与えることに成功した。さらに、高性能コード生成において鍵となる技術の１つである「オフショアリング」の実装および応用例の作成を進めた。オフショアリングは、コード生成器を記述する高レベル言語と、生成されるコードを記述する低レベル言語の橋渡しをする技術であり、現代的な高性能コードの生成においては必須とされる技術である。段階的計算を実現するプログラミング言語MetaOCamlにオフショアリング機能を標準装備することに生成するとともに、C言語へのオフショアリングに関する従来手法において変数の取り扱いに問題がある事を発見して、改善手法を提案した。

In the initial year of the study and in 2022, the calculation system of the basic stage of this study was developed, and the calculation method was used to generate the calculation method of the basic stage of this study. Special, dependent type, type The first step in research is to develop, analyze, verify and unify the application examples of code division, and improve the performance. In this study, we successfully achieved the goal of high performance computer generation by using polynomial algorithm and high performance computer. In the above note, the calculation of the order of parallelism and duplication is important, and the calculation of algebra is successful in the study of theory and practice. In addition, high-performance computer technology has been developed to improve the implementation of computer technology and application. The technology of high performance speech generation is the key to modern high performance speech generation The calculation of the stage is carried out in accordance with the requirements of the speech meta-OCaml function, the speech meta-OCaml function and the speech meta-OCaml function.

项目成果

Unified Program Generation and Verification: A Case Study on Number-Theoretic Transform

统一程序生成与验证：数论变换案例研究

• DOI: 10.1007/978-3-030-99461-7_8
• 发表时间: 2022
• 期刊: Lecture Notes in Computer Science
• 作者: S. Nakano;S. Fujita;A. Kadokura;Y. Tanaka;R. Kataoka;A. Nakamizo;K. Hosokawa;S. Saita;Masahiro Masuda and Yukiyoshi Kameyama
• 通讯作者: Masahiro Masuda and Yukiyoshi Kameyama

A Functional Abstraction of Typed Invocation Contexts

类型化调用上下文的功能抽象

• DOI: 10.46298/lmcs-18
• 发表时间: 2022
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Cong Youyou;Ishio Chiaki;Honda Kaho;Asai Kenichi
• 通讯作者: Asai Kenichi

Understanding Algebraic Effect Handlers via Delimited Control Operators

通过定界控制运算符了解代数效应处理程序

• 发表时间: 2022
• 作者: 木伏紅緒;新澤庸介;神崎素樹;Youyou Cong
• 通讯作者: Youyou Cong

Generating Programs for Polynomial Multiplication with Correctness Assurance

• DOI: 10.1145/3571786.3573017
• 发表时间: 2023-01
• 期刊: Proceedings of the 2023 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation
• 作者: Ryohei Tokuda;Yukiyoshi Kameyama

shift/reset を含む型付き言語における Reflection 証明

类型化语言的反射证明，包括移位/重置

• 发表时间: 2023
• 作者: 本田 華歩;山本 充子;浅井 健一
• 通讯作者: 浅井 健一