内涵 Martin-L"of 类型理论中余数据类型的终端语义
计算机科学中的逻辑
2014-04-23 v2 范畴论
摘要
在本工作中，我们研究了相对余单子 (relative comonad) 及其上余模 (comodule) 的概念，并利用这些概念在内涵 Martin-L"of 类型理论中，分别为流 (streams) 和无限三角矩阵的余归纳类型族给出了终端余代数语义。我们的结果已在证明助手 Coq 中实现了机械化。
引用
@article{arxiv.1401.1053,
title = {Terminal semantics for codata types in intensional Martin-L\"of type theory},
author = {Benedikt Ahrens and Régis Spadotti},
journal= {arXiv preprint arXiv:1401.1053},
year = {2014}
}
备注
14 pages, ancillary files contain formalized proof in the proof assistant Coq; v2: 20 pages, title and abstract changed, give a terminal semantics for streams as well as for matrices, Coq proof files updated accordingly