Refinement calculus for logic programming in Isabelle/HOL

4Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

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.

Cite

CITATION STYLE

APA

Hemer, D., Hayes, I., & Strooper, P. (2001). Refinement calculus for logic programming in Isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2152, pp. 249–264). Springer Verlag. https://doi.org/10.1007/3-540-44755-5_18

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free