paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Syntax and Semantics of Quantitative Type Theory

定量类型理论的语法与语义
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 该论文研究定量类型理论及其资源敏感的实现性语义，属于 PL/类型论基础理论，与用户关注的面向 ML/Agent 的静态分析、LLM 与静态分析/形式化验证交叉、浮点程序分析、贝叶斯程序分析等核心方向没有直接关联。虽然形式化程度高，但缺少与 AI/LLM 或具体程序分析场景的明确联系。引用 98 inbox
Robert Atkey
类型系统形式语义
crossref: 2026-09-12

AI 速览

一句话：提出定量类型理论，并给出基于线性组合代数与定量CwF的资源敏感实现性语义。

本文提出定量类型理论（QTT），在判断中为每个变量记录用量信息，延续 McBride 的系统。该用量信息可用于构造实现性语义：作者采用线性组合代数（Linear Combinatory Algebras）的变体，使传统类型论的实现性语义能够精确追踪资源行为。为建模这类资源敏感类型理论，论文引入定量族范畴（Quantitative Categories with Families, QCwF），作为族范畴（CwF）的新扩展，并据此定义 QTT 的语义。该工作连接了语法、用量标注与范畴语义，为资源敏感类型理论提供语义基础。

问题
如何为在判断中显式记录变量使用量的类型理论提供语义，使其准确刻画资源敏感行为。
方法
基于 McBride 的用量标注系统，使用线性组合代数变体构造实现性语义，并引入 Quantitative Categories with Families 作为语义模型。
评估
论文以语义定义与范畴模型构造作为主要论证方式，通过实现性语义说明该类型理论能够追踪资源行为。
原文摘要（Abstract）

We present Quantitative Type Theory, a Type Theory that records usage information for each variable in a judgement, based on a previous system by McBride. The usage information is used to give a realizability semantics using a variant of Linear Combinatory Algebras, refining the usual realizability semantics of Type Theory by accurately tracking resource behaviour. We define the semantics in terms of Quantitative Categories with Families, a novel extension of Categories with Families for modelling resource sensitive type theories.

链接与引用

DOI 原文 ·

BibTeX 
@inproceedings{paperbot4366,
  title = {Syntax and Semantics of Quantitative Type Theory},
  author = {Robert Atkey},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209189}
}