Refinement concepts formalised in higher order logic

DOI10.1007/BF01888227zbMATH Open0703.68074MaRDI QIDQ916409FDOQ916409

Authors: Elsie Sterbin Gottlieb 

Publication date: 1990

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

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

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)

Cites Work

• Edinburgh LCF. A mechanized logic of computation
• A lattice-theoretical fixpoint theorem and its applications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A theoretical basis for stepwise refinement and the programming calculus
• Stepwise refinement of parallel algorithms
• A calculus of refinements for program derivations
• Data refinement of predicate transformers
• Duality in specification languages: A lattice-theoretical approach
• A simple fixpoint argument without the restriction to continuity

Cited In (19)

• Program derivation using the refinement calculator
• Using lattice theory in higher order logic
• Refinement of Higher-Order Logic Programs
• Theories for mechanical proofs of imperative programs
• Understanding, Explaining, and Deriving Refinement
• Real-time refinement in Manna and Pnueli's temporal logic
• From Proposition to Program
• Mechanizing some advanced refinement concepts
• Title not available (Why is that?)
• Title not available (Why is that?)
• Refinement to Imperative/HOL
• Refinement
• A tactic language for refinement of state-rich concurrent specifications
• A specification-oriented semantics for the refinement of real-time systems
• A predicative semantics for the refinement of real-time systems
• Title not available (Why is that?)
• On refinement in rewriting logic
• Formalising general correctness
• Title not available (Why is that?)

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)