A compositional natural semantics and Hoare logic for low-level languages
From MaRDI portal
Publication:877026
DOI10.1016/J.TCS.2006.12.020zbMATH Open1111.68071OpenAlexW2170606418MaRDI QIDQ877026FDOQ877026
Publication date: 19 April 2007
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2006.12.020
Recommendations
- A compositional natural semantics and Hoare logic for low-level languages
- A compositional semantics for logic programs
- Compositional Semantics for the Procedural Interpretation of Logic
- Program Development in Computational Logic
- Compositional model-theoretic semantics for logic programs
- An approach to natural-language semantics in logic programming
- Fully abstract compositional semantics for an algebra of logic programs
- A compositional typed higher-order logic with definitions
- Consistency and axiomatization of a natural extensional combinatory logic
- Compositional natural language semantics using independence friendly logic or dependence logic
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)
Cites Work
- Title not available (Why is that?)
- An axiomatic basis for computer programming
- Soundness and Completeness of an Axiom System for Program Verification
- Certified assembly programming with embedded code pointers
- Verification, Model Checking, and Abstract Interpretation
- Axiomatic approach to side effects and general jumps
- Program proving: KJumps and functions
- A critique of the foundations of Hoare style programming logics
- Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings
- Program and proof optimizations with type systems
- Goto statements: Semantics and deduction systems
- A compositional natural semantics and Hoare logic for low-level languages
- Programming Languages and Systems
Cited In (7)
- Relational bytecode correlations
- Proof optimization for partial redundancy elimination
- Certifying assembly with formal security proofs: the case of BBS
- Program and proof optimizations with type systems
- Equational Theories of Abnormal Termination Based on Kleene Algebra
- Verification, Model Checking, and Abstract Interpretation
- Preservation of Proof Obligations from Java to the Java Virtual Machine
This page was built for publication: A compositional natural semantics and Hoare logic for low-level languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q877026)
