• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Rz: A Tool For Bringing Constructive And Computable Mathematics Closer To Programming Practice
【24h】

Rz: A Tool For Bringing Constructive And Computable Mathematics Closer To Programming Practice

机译：Rz：一种使构造性和可计算数学更接近编程实践的工具

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Readability theory is not just a fundamental tool in logic and computability. It also has direct application to the design and implementation of programs, since it can produce code interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.
机译：可读性理论不仅是逻辑和可计算性的基本工具。它也可以直接应用于程序的设计和实现，因为它可以为与数学理论相对应的数据结构生成代码接口。我们的工具称为RZ，它是建设性数学与程序设计世界之间的桥梁。通过使用构造数学的可实现性解释，RZ将构造逻辑中的规范转换为Objective Caml中的带注释的接口代码。该系统支持丰富的输入语言，允许描述复杂的数学结构。 RZ不会从证明中提取代码，但允许使用任何实现方法，从手写代码到其他工具从证明中提取的代码。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号