首页> 外文期刊>Journal of Functional Programming >Algebra of programming in Agda: Dependent types for relational program derivation
【24h】

Algebra of programming in Agda: Dependent types for relational program derivation

机译:Agda中的编程代数:关系程序派生的依赖类型

获取原文
获取原文并翻译 | 示例

摘要

Relational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties to be verified by the type checker. We have developed a library, AoPA (Algebra of Programming in Agda), to encode relational derivations in the dependently typed programming language Agda. A program is coupled with an algebraic derivation whose correctness is guaranteed by the type system. Two non-trivial examples are presented: an optimisation problem and a derivation of quicksort in which well-founded recursion is used to model terminating hylomorphisms in a language with inductive types.
机译:关系程序推导是一种通过代数规则逐步完善程序的关系规范的技术。这样获得的程序在构造上是正确的。同时,从属类型理论足够丰富,可以表达各种类型的正确性以供类型检查器验证。我们已经开发了一个库AoPA(阿格达的编程代数),以依赖类型的编程语言阿格达编码关系派生。一个程序与一个代数推导相结合,其类型系统的正确性得到了保证。给出了两个非平凡的示例:一个优化问题和一个快速排序的推导,其中使用了有根据的递归来对归纳类型的语言中的终止同构进行建模。

著录项

  • 来源
    《Journal of Functional Programming》 |2009年第5期|545-579|共35页
  • 作者单位

    Institute of Information Science, Academia Sinica, Taiwan;

    Department of Computer Science and Information Engineering, National Taiwan University, Taiwan;

    Department of Computer Science and Engineering, Chalmers University of Technology, and University of Gothenburg, Sweden;

  • 收录信息 美国《科学引文索引》(SCI);
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号