Predicate transformers and higher-order programs

DOI10.1016/0304-3975(94)00247-GMaRDI QIDQ672318zbMATH OpenFDO

Authors David A. Naumann

Publication date 28 February 1997

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(94)00247-G

zbMATH Keywords

categorial axiomatizations of program constructsHoare logicrefinement calculus

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Theory of software (68N99)

Recommendations

• Towards a calculus of predicate transformers
• A categorical model for higher order imperative programming
• Predicate transformers as power operations
• Data refinement, call by value and higher order programs
• scientific article; zbMATH DE number 3999260

Cites work

• A calculus of refinements for program derivations
• A general proof rule for procedures in predicate transformer semantics
• A generalization of Naundorf's fixpoint theorem
• A recursion theorem for predicate transformers on inductive data types
• An algebraic construction of predicate transformers
• Calculating with procedure calls
• Can programming be liberated from the von Neumann style?
• Categories, relations and dynamic programming
• Corrigenda: laws of programming
• Data refinement by calculation
• Domain theory in logical form
• Equivalence of the Gries and Martin proof rules for procedure calls
• scientific article; zbMATH DE number 3982493 (Why is no real title available?)
• scientific article; zbMATH DE number 3705887 (Why is no real title available?)
• scientific article; zbMATH DE number 3733226 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3748394 (Why is no real title available?)
• scientific article; zbMATH DE number 3787631 (Why is no real title available?)
• scientific article; zbMATH DE number 41231 (Why is no real title available?)
• scientific article; zbMATH DE number 45228 (Why is no real title available?)
• scientific article; zbMATH DE number 53111 (Why is no real title available?)
• scientific article; zbMATH DE number 107664 (Why is no real title available?)
• scientific article; zbMATH DE number 3522194 (Why is no real title available?)
• scientific article; zbMATH DE number 400814 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• Inductive data types for predicate transformers
• Local adjunctions
• On correct refinement of programs
• Pre-adjunctions in order enriched categories
• Procedures, parameters, and abstraction: Separate concerns
• Programming as a Discipline of Mathematical Nature
• Semantical analysis of specification logic
• The specification statement
• The theory of semi-functors

Cited in

(22)

• Inductive data types for predicate transformers
• A recursion theorem for predicate transformers on inductive data types
• A predicate transformer for the progress property `to-always'
• Soundness of data refinement for a higher-order imperative language
• Generic transformations of predicate encodings: constructions and applications
• Predicate transformers as power operations
• Data refinement, call by value and higher order programs
• Higher-order UTP for a theory of methods
• scientific article; zbMATH DE number 5708042 (Why is no real title available?)
• Predicate transformers for extended probability and non-determinism
• Predicative programming Part II
• Programs, Recursion and Unbounded Choice
• A categorical model for higher order imperative programming
• scientific article; zbMATH DE number 512951 (Why is no real title available?)
• scientific article; zbMATH DE number 1479646 (Why is no real title available?)
• scientific article; zbMATH DE number 1390087 (Why is no real title available?)
• Building PMCFG Parsers as Datalog Program Transformations
• Category theoretic models of data refinement
• Computer Science Logic
• Predicate transformer semantics of a higher-order imperative language with record subtyping
• Formalizing Dijkstra's predicate transformer wp in weak second-order logic
• A general proof rule for procedures in predicate transformer semantics

This page was built for publication: Predicate transformers and higher-order programs

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