Dedukti 中两层类型理论的实现及其在立方类型理论中的应用
计算机科学中的逻辑
2021-01-12 v1
摘要
在本文中，我们在将立方类型理论（CTT）编码到 Dedukti 逻辑框架方面迈出了实质性一步。CTT 表达式的类型检查具有 de Morgan 代数中的判定过程，该过程迄今无法由 Dedukti 的重写规则表达。作为替代，两层类型理论是 Martin-Löf 类型理论的变体，其中全部或部分定义等式可用所谓的外部等式表示。我们提议拆分编码：给出两层类型理论（2LTT）在 Dedukti 中的编码，以及 CTT 在 2LTT 中的部分编码。
引用
@article{arxiv.2101.03810,
title = {Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory},
author = {Bruno Barras and Valentin Maestracci},
journal= {arXiv preprint arXiv:2101.03810},
year = {2021}
}
备注
In Proceedings LFMTP 2020, arXiv:2101.02835