Please use this identifier to cite or link to this item:
https://hdl.handle.net/2440/33981
Citations | ||
Scopus | Web of ScienceĀ® | Altmetric |
---|---|---|
?
|
?
|
Type: | Journal article |
Title: | Refinement Calculus for Logic Programming in Isabelle/HOL |
Author: | Hemer, D. Hayes, I. Strooper, P. |
Citation: | Lecture Notes in Artificial Intelligence, 2001; 2152:249-264 |
Publisher: | Springer-Verlag Berlin |
Issue Date: | 2001 |
ISSN: | 0302-9743 |
Statement of Responsibility: | David Hemer, Ian Hayes, and Paul Strooper |
Abstract: | This paper describes a deep embedding of a refinement calculus for logic programs in Isabelle/HOL. It extends a previous tool with support for procedures and recursion. The tool supports refinement in context, and a number of window-inference tactics that ease the burden on the user. In this paper, we also discuss the insights gained into the suitability of different logics for embedding refinement calculii (applicable to both declarative and imperative paradigms). In particular, we discuss the richness of the language, choice between typed and untyped logics, automated proof support, support for user-defined tactics, and representation of program states. |
Description: | The original publication can be found at www.springerlink.com |
DOI: | 10.1007/3-540-44755-5_18 |
Published version: | http://www.springerlink.com/content/3g698f5eqc9dugxj/ |
Appears in Collections: | Aurora harvest Computer Science publications |
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.