一个计算机验证的、单子式的、函数式的积分实现
A computer verified, monadic, functional implementation of the integral
Radboud University Nijmegen（奈梅亨拉德堡德大学）
AI总结：
本文在类型论中实现了黎曼积分的计算机验证的精确单子式函数式实现，结合O'Connor先前的工作，标志着Bishop将构造性数学用作精确分析编程语言的愿景的开端。
摘要：
我们在类型论中提供了黎曼积分的计算机验证的精确单子式函数式实现。结合O'Connor先前的工作，这可以看作是Bishop将构造性数学用作精确分析编程语言的愿景的开端。
英文摘要：
We provide a computer verified exact monadic functional implementation of the Riemann integral in type theory. Together with previous work by O'Connor, this may be seen as the beginning of the realization of Bishop's vision to use constructive mathematics as a programming language for exact analysis.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
