Refinement of higher-order logic programs

被引：1
|
作者：
Colvin, R [1 ]
Hayes, I [1 ]
Hemer, D [1 ]
Strooper, P [1 ]
机构：
[1] Univ Queensland, Sch Informat Technol & Elect Engn, Brisbane, Qld 4072, Australia
来源：
LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION | 2003年 / 2664卷
关键词：
D O I：
10.1007/3-540-45013-0_11
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we extend the refinement calculus for logic programs to include higher-order programming capabilities in specifications and programs, such as procedures as terms and lambda abstraction. We use a higher-order type and term system to describe programs, and provide a semantics for the higher-order language and refinement. The calculus is illustrated by refinement examples.
引用
收藏
页码：126 / 143
页数：18
相关论文
共 50 条
  • [1] Learning higher-order logic programs
    Andrew Cropper
    Rolf Morel
    Stephen Muggleton
    [J]. Machine Learning, 2020, 109 : 1289 - 1322
  • [2] Learning higher-order logic programs
    Cropper, Andrew
    Morel, Rolf
    Muggleton, Stephen
    [J]. MACHINE LEARNING, 2020, 109 (07) : 1289 - 1322
  • [3] Higher-order transformation of logic programs
    Seres, S
    Spivey, M
    [J]. LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2001, 2042 : 57 - 68
  • [4] A relational logic for higher-Order programs
    Aguirre A.
    Barthe G.
    Gaboardi M.
    Garg D.
    Strub P.-Y.
    [J]. 2017, Association for Computing Machinery (01)
  • [5] A relational logic for higher-order programs
    Aguirre, Alejandro
    Barthe, Gilles
    Gaboardi, Marco
    Garg, Deepak
    Strub, Pierre-Yves
    [J]. JOURNAL OF FUNCTIONAL PROGRAMMING, 2019, 29
  • [6] Proving pointer programs in higher-order logic
    Mehta, F
    Nipkow, T
    [J]. AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 121 - 135
  • [7] A Temporal Logic for Higher-Order Functional Programs
    Okuyama, Yuya
    Tsukada, Takeshi
    Kobayashi, Naoki
    [J]. STATIC ANALYSIS (SAS 2019), 2019, 11822 : 437 - 458
  • [8] Proving pointer programs in higher-order logic
    Mehta, F
    Nipkow, T
    [J]. INFORMATION AND COMPUTATION, 2005, 199 (1-2) : 200 - 227
  • [9] Logic-flow analysis of higher-order programs
    Might, Matthew
    [J]. ACM SIGPLAN NOTICES, 2007, 42 (01) : 185 - 198
  • [10] Propositional Dynamic Logic for Higher-Order Functional Programs
    Satake, Yuki
    Unno, Hiroshi
    [J]. COMPUTER AIDED VERIFICATION (CAV 2018), PT I, 2018, 10981 : 105 - 123
12345