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

用于在存在各种计算效果的情况下验证时间和状态相关属性的类型系统

• 批准号: 22K17875
• 负责人: 関山 太朗
• 金额: $ 3万
• 依托单位: National Institute of Informatics
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Early-Career Scientists
• 财政年份: 2022
• 资助国家: 日本
• 起止时间: 2022-04-01 至 2025-03-31
• 项目状态: 未结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-22K17875/
• 关键词: プログラミング言語; 型システム; 計算効果; 時相的検証; 形式検証

2022年度は限定継続演算子を利用するプログラムの時相的性質を検証するための手法について研究を行った。限定継続演算子は限定継続と呼ばれる、一種のプログラム文脈を値として取り出すことのできる命令で、これを利用することで例外、バックトラック、ジェネレーターなどの、計算効果を引き起こす様々なプログラミング機能が実装できることが知られている。そのためこの命令を扱えるような検証手法を与えることで、上記に挙げたプログラミング機能を利用するプログラムの性質を検証することが可能となる。2022年度はshift0/resetと呼ばれる限定継続演算子に対し、時相的性質を検証するための型理論を構築し、検証手法実装への足がかりを掴んだ。また今回の手法を応用することで、エフェクトハンドラと呼ばれる別種の限定継続演算子に対して依存篩型による正確な検証を可能にする型理論を構築することにも成功した。さらに限定演算子の利用を前提とした時相的検証の研究を通して、より一般的な再帰型を用いるプログラムを対象とした時相的検証に関する知見を得ることができた。

2022 年，我们对验证使用有限延续运算符的程序的时间属性的方法进行了研究。有限延续运算符称为有限延续，是一种可以将程序上下文提取为值的指令。通过使用该运算符，可以实现异常、回溯、生成器等引起计算效果的各种编程函数。已实施。因此，通过提供能够处理该指令的验证方法，可以验证使用上面列出的编程功能的程序的属性。 2022 年，我们构建了一种类型理论，用于验证名为 shift0/reset 的有限延续运算符的时间属性，并在实现验证方法方面取得了立足点。此外，通过应用这种方法，我们成功地构建了一种类型理论，该理论能够使用依赖筛类型对另一种类型的有限延续运算符（称为效果处理程序）进行精确验证。此外，通过对假设使用限制性运算符的时间验证的研究，我们能够获得有关使用更通用的递归类型的程序的时间验证的知识。

项目成果

代数的エフェクトとハンドラのためのエフェクトシステムの抽象化

代数效应和处理程序的效应系统抽象

• 发表时间: 2023
• 作者: 吉岡 拓真;関山 太朗;五十嵐 淳
• 通讯作者: 五十嵐 淳

計算効果入門 ― プログラミングから理論まで ―

计算效应简介——从编程到理论——

• 发表时间: 2022
• 作者: 関山 太朗;勝股 審也;叢 悠悠
• 通讯作者: 叢 悠悠

Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations

具有答案效果修改的时间验证：具有定界延续的依赖时间类型和效果系统

• DOI: 10.1145/3571264
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Sekiyama Taro;Unno Hiroshi
• 通讯作者: Unno Hiroshi

限定継続のための高階プログラム論理

用于有限延续的高阶程序逻辑

• 发表时间: 2023
• 作者: 佐藤 惇;関山 太朗;五十嵐 淳
• 通讯作者: 五十嵐 淳

代数的エフェクトハンドラのための篩型システム

用于代数效应处理程序的筛选系统

• 发表时间: 2023
• 作者: 川俣 楓河;海野 広志;関山 太朗;寺内 多智弘
• 通讯作者: 寺内 多智弘