摘要：用Minlog证明助手生成正式证明并提取其计算内容，作为有限或无限数据的类型理论的术语的形式，描述了一些对提取术语进行转换为Haskell之后的运行的实验。
作者：Helmut Schwichtenberg, Franziskus Wiesnet
论文ID：1904.12763
分类：Logic
分类简称：math.LO
提交时间：2023-06-22
PDF 下载： 英文版 中文版pdf翻译中