paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Extensional and Intensional Semantic Universes

外延与内涵语义宇宙
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 1/10 · 该论文属于纯类型论与指称语义研究，讨论内涵/外延语义宇宙和图博弈模型，与用户关注的 LLM/Agent 静态分析、浮点程序分析、贝叶斯程序分析及其与 LLM 的交叉均无直接关联；虽属 PL 形式语义，但并非研究方向核心。引用 2 inbox
Valentin Blot, Jim Laird
形式语义
crossref: 2026-09-12

AI 速览

一句话：提出一种同时包含内涵与外延语义宇宙的依赖类型理论及其指称模型，其中项与类型分别解释为图博弈策略和事件域上的稳定函数。

本文研究如何为同时包含内涵与外延语义视角的依赖类型理论提供统一指称语义。作者提出一个依赖类型理论并构造其指称模型：在内涵语义宇宙中，项和类型被解释为特定图博弈上的策略，这些策略对应广义形式的具象数据结构；在外延语义宇宙中，它们则被解释为事件域上的稳定函数。通过在同一类型理论中同时容纳这两类解释，论文给出了一个可同时描述内涵与外延语义的理论框架。摘要未报告实现或实验评估，主要贡献是类型理论与指称模型的理论构造。

问题
如何为同时包含内涵与外延语义宇宙的依赖类型理论建立统一的指称语义。
方法
构造一个依赖类型理论及其指称模型，内涵侧将项和类型解释为图博弈策略，外延侧将其解释为事件域上的稳定函数。
评估
摘要未给出实验或机器化验证；评估体现为所提出类型理论与指称模型的理论构造与一致性说明。
原文摘要（Abstract）

We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot4351,
  title = {Extensional and Intensional Semantic Universes},
  author = {Valentin Blot and Jim Laird},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209206}
}