一句话：提出基于幺半范畴纤维化的线性依赖类型论，并将其集成到量子电路语言 Proto-Quipper-M。
现代量子编程语言需同时支持量子资源与经典控制：线性类型可刻画不可克隆，而依赖类型可表达由经典参数索引的电路族，因此需要线性依赖类型论。本文通过幺半范畴的某些纤维化定义此类类型论的通用语义结构，并指出 Rios 与 Selinger 的 Proto-Quipper-M 的范畴模型正是该纤维化的一个实例，从而可将依赖类型集成进该语言。作者进一步设计了一个通用线性依赖类型系统，以及 Proto-Quipper-M 的依赖类型扩展，给出操作语义和原型实现，为量子电路描述语言的依赖类型化提供了语义基础与语言实例。
Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M by Rios and Selinger (2017) constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.
@article{paperbot1657,
title = {Linear Dependent Type Theory for Quantum Programming Languages},
author = {Peng Fu and Kohei Kishida and Peter Selinger},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:28)2022}
}