Game semantics and intersection type systems for program verification

用于程序验证的游戏语义和交集类型系统

• 批准号: 16K16004
• 负责人: Tsukada Takeshi
• 金额: $ 1.83万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2016
• 资助国家: 日本
• 起止时间: 2016-04-01 至 2019-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-16K16004/
• 关键词: ゲーム意味論; 交差型システム; generalised species; 線形論理; プログラム意味論; 微分λ計算; π計算; プログラム検証

项目成果

Species, Profunctors and Taylor Expansion Weighted by SMCC

SMCC 加权的物种、函子和泰勒展开式

• DOI: 10.1145/3209108.3209157
• 发表时间: 2018
• 期刊: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
• 作者: Takeshi Tsukada;Kazuyuki Asada;C.-H. Luke Ong
• 通讯作者: C.-H. Luke Ong

Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence

几乎每个简单键入的 $$lambda $$-Term 都有一个很长的 $$eta $$-Reduction 序列

• DOI: 10.1007/978-3-662-54458-7_4
• 发表时间: 2017
• 期刊: Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures
• 作者: Sin’ya Ryoma;Asada Kazuyuki;Kobayashi Naoki and Tsukada Takeshi
• 通讯作者: Kobayashi Naoki and Tsukada Takeshi

Plays as Resource Terms via Non-idempotent Intersection Types

通过非幂等交集类型充当资源项

• DOI: 10.1145/2933575.2934553
• 发表时间: 2016
• 期刊: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
• 作者: Naonori Kakimura;Naoyuki Kamiyama;Kenjiro Takazawa;Takeshi Tsukada and C.-H. Luke Ong
• 通讯作者: Takeshi Tsukada and C.-H. Luke Ong

Strategies in HO/N games as profunctors

HO/N 博弈中作为函子的策略

• 发表时间: 2016
• 作者: Naonori Kakimura;Naoyuki Kamiyama;and Kenjiro Takazawa;Kazuyuki Asada and Takeshi Tsukada
• 通讯作者: Kazuyuki Asada and Takeshi Tsukada

A Categorical Model of an $$\mathbf {i/o}$$ -typed $$\pi $$ -calculus

$$mathbf {i/o}$$ 型 $$pi $$ 微积分的分类模型

• DOI: 10.1007/978-3-030-17184-1_23
• 发表时间: 2019
• 期刊: Proceedings of the 28th European Symposium on Programming
• 作者: Sakayori Ken;Tsukada Takeshi
• 通讯作者: Tsukada Takeshi