摘要：用存在于整数上的超滤器的证明，我们展示了如何将经典分析中的证明转化为程序。该方法混合了作者引入的经典实现与P.Cohen的"强行"方法。我们得到的程序使用了随机访问内存中的读取和写入指令。
作者：Jean-Louis Krivine (PPS)
论文ID：0809.2394
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-09-16
PDF 下载： 英文版 中文版pdf翻译中