Design and development of multi-stage languages for verification

用于验证的多阶段语言的设计和开发

• 批准号: 15K12007
• 负责人: KAMEYAMA YUKIYOSHI
• 金额: $ 2.25万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Challenging Exploratory Research
• 财政年份: 2015
• 资助国家: 日本
• 起止时间: 2015-04-01 至 2018-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-15K12007/
• 关键词: 証明記述言語; プログラム生成; メタプログラミング; コントロールエフェクト; 副作用; 型安全性; モジュール; 定理証明支援システム; プログラム抽出・生成; 型システム; スコープ安全性; 定理証明系; 形式検証; 証明の自動化; プログラム抽出; 証明探索; 証明の生成

项目成果

Answer-Type Modification without Tears: Prompt-Passing Style Translation for Typed Delimited-Control Operators

无泪的答案类型修改：类型化分隔控制运算符的提示传递风格翻译

• 发表时间: 2016
• 期刊: Post-conference Proceedings of Workshop on Continuations 2015, EPTCS
• 作者: Ikuo Kobori;Yukiyosih Kameyama;Oleg Kiselyov
• 通讯作者: Oleg Kiselyov

Refined Environment Classifiers: Type- and Scope-safe Code Generation with Mutable Cells

细化环境分类器：使用可变单元生成类型和范围安全的代码

• DOI: 10.1007/978-3-319-47958-3_15
• 发表时间: 2016
• 期刊: Proceedings of Asian Symposium on Programming Languages and Systems
• 作者: Oleg Kiselyov;Yukiyoshi Kameyama;Yuto Sudo
• 通讯作者: Yuto Sudo

Type-Safe Multi-Stage Programming with Control

带控制的类型安全多阶段编程

• 发表时间: 2017
• 作者: 薄井千春;亀山幸義;Yukiyoshi Kameyama
• 通讯作者: Yukiyoshi Kameyama

定理証明器Coqの効率t系な有限ドメイン関数

定理证明器 Coq 的效率 t 系统有限域函数

• 发表时间: 2017
• 期刊: 情報処理学会論文誌：プログラミング
• 作者: 坂口和彦;亀山幸義
• 通讯作者: 亀山幸義

多段階 let 挿入を行うコード生成言語の型システムの設計

为具有多级let插入的代码生成语言设计类型系统

• 发表时间: 2016
• 作者: 大石純平;亀山幸義
• 通讯作者: 亀山幸義