Quipper量子编程语言元理论在线性逻辑中的形式化
计算机科学中的逻辑
2018-12-11 v1 编程语言
摘要
我们在Hybrid系统中开发了一个线性逻辑框架，并用其推理量子lambda演算的类型系统。具体而言，我们考虑该演算的一个实用版本Proto-Quipper，其包含Quipper的核心。Quipper是一种新兴的量子编程语言，正处于活跃开发中，近期在量子计算界广受欢迎。Hybrid是一个支持在Coq证明辅助工具中使用高阶抽象语法（HOAS）来表示和推理形式化系统的系统。本工作中，我们通过扩展该系统加入线性规范逻辑（SL），以推理Quipper的线性类型系统。为此，我们在SL中编码Proto-Quipper的语义（即类型规则与求值规则），并证明类型安全性。
引用
@article{arxiv.1812.03624,
title = {Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic},
author = {Mohamed Yousri Mahmoud and Amy P. Felty},
journal= {arXiv preprint arXiv:1812.03624},
year = {2018}
}
备注
40 pages, 5 figures