论文标题
关于电路说明语言中的动态提升和效果键入（扩展版本）
On Dynamic Lifting and Effect Typing in Circuit Description Languages (Extended Version)
论文作者
论文摘要
在量子计算领域，电路描述语言代表了传统QRAM式语言的有效替代方案。它们确实可以在不牺牲灵活性或模块化的情况下对输出电路进行更精细的控制。我们介绍了范式lambda-calculus proto-Quipper-M的概括，本身对量子电路说明语言震动的核心特征进行建模。该扩展名为Proto-Quipper-K，旨在捕获一种非常通用的动态提升形式。通过引入丰富的类型和效果系统，这不仅是计算，而且类型都是有效的。我们为引入语言给出的主要结果是经典的声音结果，即减少和进步。
In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. They indeed allow for finer control over the output circuit, without sacrificing flexibility nor modularity. We introduce a generalization of the paradigmatic lambda-calculus Proto-Quipper-M, itself modeling the core features of the quantum circuit description language Quipper. The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting. This is made possible by the introduction of a rich type and effect system in which not only computations, but also the very types are effectful. The main results we give for the introduced language are the classic type soundness results, namely subject reduction and progress.
