概率性按推值调用
摘要：添加了一个“翻转硬币”布尔闭合原子表达式的Levy的Call-By-Push-Value的概率扩展介绍了。该语言可以理解为Scott的PCF的重要概括，包括按名称调用和按值调用，并具有递归（可能惰性）数据类型。我们使用以前引入的概率一致空间的指称模型解释该语言，这是完全的经典线性逻辑的范畴模型，将数据类型解释为资源共代数。我们证明了适度性和完全抽象性，将之前的结果普遍推广到一个更加现实和强大的编程语言中。
作者：Thomas Ehrhard and Christine Tasson
论文ID：1607.04690
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22