Refinement concepts formalised in higher order logic

DOI10.1007/BF01888227MaRDI QIDQ916409zbMATH OpenFDO

Authors Elsie Sterbin Gottlieb

Publication date 1990

Published in Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

refinement calculusweakest preconditionmechanical theorem provingprogram development

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Mechanizing some advanced refinement concepts
• scientific article; zbMATH DE number 1303996
• Refinement of Higher-Order Logic Programs
• A calculus of refinements for program derivations
• scientific article; zbMATH DE number 2110621

Cites work

• scientific article; zbMATH DE number 3705887 (Why is no real title available?)
• scientific article; zbMATH DE number 3714908 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• A calculus of refinements for program derivations
• A lattice-theoretical fixpoint theorem and its applications
• A simple fixpoint argument without the restriction to continuity
• A theoretical basis for stepwise refinement and the programming calculus
• Data refinement of predicate transformers
• Duality in specification languages: A lattice-theoretical approach
• Edinburgh LCF. A mechanized logic of computation
• Stepwise refinement of parallel algorithms

Cited in

(19)

• Real-time refinement in Manna and Pnueli's temporal logic
• Mechanizing some advanced refinement concepts
• From proposition to program. Embedding the refinement calculus in Coq
• On refinement in rewriting logic
• Refinement of Higher-Order Logic Programs
• scientific article; zbMATH DE number 1670754 (Why is no real title available?)
• Formalising general correctness
• A specification-oriented semantics for the refinement of real-time systems
• Refinement to Imperative/HOL
• A tactic language for refinement of state-rich concurrent specifications
• Refinement
• Theories for mechanical proofs of imperative programs
• A predicative semantics for the refinement of real-time systems
• Understanding, Explaining, and Deriving Refinement
• scientific article; zbMATH DE number 1424020 (Why is no real title available?)
• Program derivation using the refinement calculator
• Using lattice theory in higher order logic
• scientific article; zbMATH DE number 1303996 (Why is no real title available?)
• scientific article; zbMATH DE number 1863386 (Why is no real title available?)

Describes a project that uses

Uses Software

• HOL

This page was built for publication: Refinement concepts formalised in higher order logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q916409)