Development of theory and application of programming based on higher-order/typed calculi

基于高阶/类型演算的编程理论和应用的发展

• 批准号: 15H02681
• 负责人: Sumii Eijiro
• 金额: $ 11.4万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2015
• 资助国家: 日本
• 起止时间: 2015-04-01 至 2020-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15H02681/
• 关键词: プログラミング言語理論; 関数型プログラミング; 高階計算・λ計算（ラムダ計算）; 型システム; 情報セキュリティ・情報流解析; 並行・分散計算; 形式的（機械的）定理証明・検証; 環境双模倣; セキュリティ; 並行計算; ソフトウェア基礎; 関数型言語; 必要呼び評価戦略; 関数型プログラミング言語; セキュリティ型つきλ計算; 非機密化(declassification); 遅延評価; 名前呼び; 必要呼び; プログラム検証; 評価戦略; λ計算; セキュリ

项目成果

無限の入出力を行う関数型プログラムのK正規化の形式的検証

具有无限输入/输出的函数程序的 K 归一化的形式验证

• 发表时间: 2017
• 作者: 水野 雅之; 住井 英二郎
• 通讯作者: 住井 英二郎

Call/ccを含む型無しラムダ計算における文脈等価性の一証明手法

一种在无类型 lambda 计算（包括 call/cc）中证明上下文等价的方法

• 发表时间: 2015
• 作者: 谷内太一;住井英二郎
• 通讯作者: 住井英二郎

Formal Verification of the Correspondence between Call-by-Need and Call-by-Name

Call-by-Need 和 Call-by-Name 之间对应关系的形式验证

• 发表时间: 2018
• 作者: Masayuki Mizuno; Eijiro Sumii
• 通讯作者: Eijiro Sumii

Specialization of Generic Array Accesses After Inlining

内联后通用数组访问的专门化

• DOI: 10.4204/eptcs.241.4
• 发表时间: 2017
• 作者: Ryohei Tokuda; Eijiro Sumii; Akinori Abe
• 通讯作者: Akinori Abe

機械学習による関数型ブーリアンプログラムの型推論

使用机器学习进行函数式布尔程序的类型推断

• 发表时间: 2016
• 作者: 阿部 晃典;住井 英二郎
• 通讯作者: 住井 英二郎