Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1007/3-540-45013-0_11 | LOPSTR |
Keywords | Field | DocType |
higher-order logic program,term system,lambda abstraction,higher-order language,higher-order type,refinement calculus,higher-order programming capability,refinement example,logic program,higher order,higher order logic | Programming language,Refinement calculus,Computer science,Correctness,Type theory,Algorithm,Theoretical computer science,Refinement,Semantics,Higher-order logic,Type constructor,Executable | Conference |
Volume | ISSN | ISBN |
2664 | 0302-9743 | 3-540-40438-4 |
Citations | PageRank | References |
1 | 0.36 | 9 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Robert Colvin | 1 | 68 | 8.67 |
| Ian Hayes | 2 | 21 | 2.71 |
| David Hemer | 3 | 19 | 2.86 |
| Paul Strooper | 4 | 701 | 68.70 |