Semantics and reasoning with free procedures

DOI10.1016/0304-3975(92)90387-UzbMath0769.68095OpenAlexW2083801902MaRDI QIDQ1193855

Steven M. German

Publication date: 27 September 1992

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

Full work available at URL: https://doi.org/10.1016/0304-3975(92)90387-u

zbMATH Keywords

reasoningsemanticsproof systeminterpretationdenotational constructionsprograms with procedures

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reasoning about procedures as parameters in the language L4
• First-order dynamic logic
• A necessary and sufficient condition in order that a Herbrand interpretation be expressive relative to recursive programs
• Effective Axiomatizations of Hoare Logics
• Soundness and Completeness of an Axiom System for Program Verification
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems

This page was built for publication: Semantics and reasoning with free procedures