计算按值调用的线性-非线性模型的计算机λ演算（扩展摘要）
摘要：线性λ演算是Selinger和Valiron开发出来的一种用于量子计算的函数式编程语言的基础。该λ演算具有线性类型系统和可重复操作符“!”。与此同时，它还采用按值调用的约减策略，并使用副作用来模拟概率测量。操作符“!”构成了一个共余子，类似于Seely，Bierman和Benton提出的线性逻辑模型。副作用构成了一个单子，类似于Moggi的计算λ演算。本文探讨了单子和共余子的组合，展示了我们的范畴语义理论的准确性和完备性。
作者：Peter Selinger (1), Beno^it Valiron (2) ((1) Dalhousie University, (2) University of Ottawa)
论文ID：0801.0813
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-01-08