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と呼ばれる限定継続演算子に対し、時相的性質を検証するための型理論を構築し、検証手法実装への足がかりを掴んだ。また今回の手法を応用することで、エフェクトハンドラと呼ばれる別種の限定継続演算子に対して依存篩型による正確な検証を可能にする型理論を構築することにも成功した。さらに限定演算子の利用を前提とした時相的検証の研究を通して、より一般的な再帰型を用いるプログラムを対象とした時相的検証に関する知見を得ることができた。

In 2022, we will conduct research on the use of finite element algorithms and the nature of time phases. The limit operator defines the context of a call, a command, an exception, a function, a calculation result, and a function. This is the first time that a person has ever used a command to verify the nature of a command. In 2022, the shift0/reset algorithm was used to determine the nature of the time phase. The model theory was constructed and the verification method was implemented. The method used in this paper is to construct a new type of theory for the identification of the correct type of dependent screening algorithm. The research on the application of the limited algorithm to the time-phase detection is conducted in a general way, and the application of the limited algorithm to the time-phase detection is conducted in a general way.

项目成果

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

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

• 发表时间: 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
• 作者: 川俣 楓河;海野 広志;関山 太朗;寺内 多智弘
• 通讯作者: 寺内 多智弘