Paper Info
Title
Abstraction and Refinement in Higher Order Logic
Abstract
We develop within higher order logic (HOL) a general and flexible method of abstraction and refinement, which specifically addresses the problem of handling constraints. We provide a HOL interpretation of first-order Lax Logic, which can be seen as a modal extension of deliverables. This provides a new technique for automating reasoning about behavioural constraints by allowing constraints to be associated with, but formally separated from, an abstracted model.We demonstrate a number of uses, e.g. achieving a formal separation of the logical and timing aspects of hardware design, and systematically generating timing constraints for a simple sequential device from a formal proof of its abstract behaviour. The method and proofs have been implemented in Isabelle as a definitional extension of the HOL logic which extends work by Jacobs and Melham on encoding dependent types in HOL. We assume familiarity with HOL but not detailed knowledge of circuit design.
Year
DOI
Venue
2001
10.1007/3-540-44755-5_15
TPHOLs
Keywords
Field
DocType
hol logic,formal proof,circuit design,higher order logic,hardware design,definitional extension,hol interpretation,flexible method,modal extension,formal separation
HOL,Logical conjunction,Abstraction,Computer science,Automated theorem proving,Algorithm,Theoretical computer science,Mathematical proof,Higher-order logic,Formal proof,Formal verification
Conference
ISBN
Citations 
PageRank 
3-540-42525-X
3
0.44
References 
Authors
8
3
Name
Order
Citations
PageRank
Matt Fairtlough1716.75
Michael Mendler231434.60
Xiaochun Cheng331.11