函数式珍宝：见证我——构造性论证须以具体见证引导
编程语言
2021-03-24 v1 计算机科学中的逻辑
摘要
备受喜爱的 Curry--Howard 对应告诉我们，类型是直觉主义命题，并且在构造数学中，命题的证明可被视为某种构造或见证，传达命题的信息。我们展示了这一视角作为开发依赖类型程序的指导原则是多么有用。
关键词
引用
@article{arxiv.2103.11751,
title = {Functional Pearl: Witness Me -- Constructive Arguments Must Be Guided with Concrete Witness},
author = {Hiromi Ishii},
journal= {arXiv preprint arXiv:2103.11751},
year = {2021}
}
备注
Submitted to Haskell'21