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言語へのオフショアリングに関する従来手法において変数の取り扱いに問題がある事を発見して、改善手法を提案した。

在研究的第一年，我们研究了诸如计算资源（内存量等）以及构成本研究基础的阶级计算系统中生成的代码的规模和性能等事项的计划生成技术和示例。特别是，我们详细介绍了基于这些定量信息的这些定量信息的成功示例，并在不使用依赖类型的传统类型系统中对这些定量信息进行了程序分析和验证。这样的研究是Kameyama和其他人开发的计划生成，分析和验证的统一框架，并进一步完善了加密字段中应用程序的示例以提高性能。特别是，尽管通常仅实施数值转换函数，但本研究成功地实现了创建高性能代码并验证其正确性，以诸如多项式乘法等较大的功能。与上述同时，我们对计算效应进行了理论和实施研究，这些研究在逐步计算中很重要，以避免代码重复，并成功阐明了代数效应与有限的连续性控制操作员之间的关系，并为有限的连续性控制器提供了统一的类型系统。此外，我们已经继续进行实施和应用程序示例“离岸”，这是生成高性能代码的关键技术之一。离岸设备是一项桥接高级语言，用于编写代码生成器和编写生成代码的低级语言，并且是一项对于生成现代高性能代码至关重要的技术。程序员创建的程序荟萃摄像机实现了逐步计算，该程序配备了离岸功能作为标准功能，并发现在传统方法中处理变量的传统方法的离岸传输方式存在问题，并提出了一种改进方法。

项目成果

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

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
• 作者: 本田 華歩;山本 充子;浅井 健一
• 通讯作者: 浅井 健一

Understanding Algebraic Effect Handlers via Delimited Control Operators

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

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