我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：将泛代数扩展为同时支持代数排序与变量绑定的框架，为简单类型理论提供代数模型。

本文研究简单类型理论的代数模型，目标是给出一个统一的代数语义框架。作者将 universal algebra 加以扩展，使其能够同时容纳 algebraic sorting 与 variable binding，从而把类型理论中的排序结构和绑定结构纳入同一套代数模型。该框架可应用于多类简单类型理论，包括无类型 λ 演算、简单类型 λ 演算、计算 λ 演算以及谓词逻辑。其核心贡献在于提出这一推广框架，并在泛代数与类型理论语义之间建立联系，为带变量绑定的简单类型理论提供代数模型工具。

问题

如何为简单类型理论建立统一的代数模型，尤其是同时处理代数排序与变量绑定这两种结构。

方法

扩展 universal algebra，提出一个同时包含 algebraic sorting 和 variable binding 的代数模型框架。

评估

通过无类型/简单类型 λ 演算、计算 λ 演算与谓词逻辑等例子展示该框架的适用范围。

链接与引用

DOI 原文 · PDF（开放获取） ·

@inproceedings{paperbot5508,
  title = {Algebraic models of simple type theories},
  author = {Nathanael Arkor and Marcelo Fiore},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394771}
}