连接演算中的代数模式匹配

将连接演算映射到异构硬件

Mapping the Join Calculus to Heterogeneous Hardware

由于现代架构引入了额外的异构性和并行性，我们寻找方法来处理这个问题，而不涉及专门的软件到每个平台。在本文中，我们采取了连接演算，并发计算的一个优雅的模型，并展示了它如何可以映射到一个架构的笛卡尔积风格的建设，从而利用演算的固有的非确定性编码的位置选择。这将放置和调度的概念统一到单个任务中。

A Diagrammatic Calculus for Algebraic Effects

We introduce a new diagrammatic notation for representing the result of (algebraic) effectful computations. Our notation explicitly separates the effects produced during a computation from the possible values returned, this way simplifying the extension of definitions and results on pure computations to an effectful setting. Additionally, we show a number of algebraic and order-theoretic laws on diagrams, this way laying the foundations for a diagrammatic calculus of algebraic effects. We give a formal foundation for such a calculus in terms of Lawvere theories and generic effects.

作用域效应与处理程序的演算

A Calculus for Scoped Effects & Handlers

针对函数式编程中作用域效应缺乏原生支持的问题，提出λₛc演算，原生支持代数与作用域效应及处理程序，扩展行多态性并提供多态处理程序和显式子句，填补了相关演算空白。

带尺寸标注的代数结构演算中类型检验的判定性

Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations

自从Val Tannen的先驱工作简单类型的类演算和一阶重写的组合（LICS'88），许多作者都通过将其扩展到更丰富的类型类演算和重写范式，最终在演算像代数结构的演算。这些工作提供了理论基础的类型理论的证明助手的功能和谓词定义的定向高阶方程。这种定义包含了基于归纳的定义，更容易编写，并提供了更多的自动化。另一方面，检查用户定义的重写规则是强规范化和融合的，并且在与beta约简结合时保持类型检查的可判定性，则更加困难。大多数终止标准依赖于期限结构。在以前的工作中，我们扩展到依赖类型和高阶重写，“大小类型”的概念由几位作者在ML类语言的简单框架中研究，并证明了它保持了强规范化。本文件的主要贡献是双重的。首先，证明了在带尺寸标注的代数构造演算中，只要尺寸标注所产生的约束集是可满足的，并且允许最一般的解，则类型推断和类型检验问题是可判定的.其次，我们证明了一个大小代数足够丰富的捕获通常的归纳为基础的定义和更多的后来的属性。

Lineal：一个线性代数Lambda演算

Lineal: A linear-algebraic Lambda-calculus

我们提供了向量空间和双线性函数的概念的计算定义。我们使用这个结果来介绍一个最小的语言相结合的高阶计算和线性代数。这种语言扩展了λ演算，使之有可能进行α t + β u项的任意线性组合。我们描述了如何“执行”这个语言的一些重写规则，并证明他们通过两个基本要求，语言是一个语言的线性运算符，它是高阶。我们提到的角度，这项工作在量子计算领域，其电路，我们可以很容易地编码在微积分。最后，我们证明了整个演算的汇合。

Parallel Algebraic Effect Handlers

Algebraic effects and handlers support composable and structured control-flow abstraction. However, existing designs of algebraic effects often require effects to be executed sequentially. This paper studies parallel algebraic effect handlers. In particular, we formalize λp, an untyped lambda calculus which models two key features, effect handlers and parallelizable computations, the latter of which takes the form of a for expression as inspired by the Dex programming language. We present various interesting examples expressible in our calculus, and provide a Haskell implementation. We hope th…