Refinement Calculus for Logic Programming in Isabelle/HOL
Date
2001
Authors
Hemer, D.
Hayes, I.
Strooper, P.
Editors
Advisors
Journal Title
Journal ISSN
Volume Title
Type:
Journal article
Citation
Lecture Notes in Artificial Intelligence, 2001; 2152:249-264
Statement of Responsibility
David Hemer, Ian Hayes, and Paul Strooper
Conference Name
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.
School/Discipline
Dissertation Note
Provenance
Description
The original publication can be found at www.springerlink.com