A Mechanically Assisted Constructive Proof in Category Theory
A Mechanically Assisted Constructive Proof in Category Theory
复制标题
范畴论中机械辅助的构造性证明
DOI：
--
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
P. Panangaden
中科院分区：
文献类型：
--
作者：
James A. Altucher;P. Panangaden
最近，范畴论、构造型论和函数式程序设计的思想有了很大的融合。我们的目标是开发一个工具包，提供机械辅助，将范畴论定理的建设性证明放在一起，并从结果中提取可执行程序。
Recently there has been a significant confluence of ideas from category theory, constructive type theory and functional programming. Our goal is to develop a toolkit that provides mechanical assistance in putting together constructive proofs of theorems in category theory and to extract executable programs from the result.