An observationally complete program logic for imperative higher-order functions
DOI10.1016/J.TCS.2013.11.003zbMATH Open1358.68071OpenAlexW1661340274MaRDI QIDQ387994FDOQ387994
Authors: Kohei Honda, Nobuko Yoshida, Martin Berger 
Publication date: 18 December 2013
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2013.11.003
Recommendations
- Descriptive and Relative Completeness of Logics for Higher-Order Functions
- A logical analysis of aliasing in imperative higher-order functions
- Relative completeness for logics of functional programs
- A logical analysis of aliasing in imperative higher-order functions
- Logical Reasoning for Higher-Order Functions with Local State
completenessobservational equivalencecharacteristic formulaehigher-order functionimperative programmingprogram logic
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cites Work
- Edinburgh LCF. A mechanized logic of computation
- Program verification through characteristic formulae
- On full abstraction for PCF: I, II and III
- Full abstraction for PCF
- Algebraic laws for nondeterminism and concurrency
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Semantical analysis of specification logic
- Characteristic formulae for the verification of imperative programs
- An axiomatic basis for computer programming
- Separation and information hiding
- Ten Years of Hoare's Logic: A Survey—Part I
- Title not available (Why is that?)
- Soundness and Completeness of an Axiom System for Program Verification
- Title not available (Why is that?)
- Types and programing languages
- Title not available (Why is that?)
- Equivalence in functional languages with effects
- Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
- Sound and complete Hoare-like calculi based on copy rules
- A sound and relatively* complete Hoare-logic for a language with higher type procedures
- Axiomatic approach to side effects and general jumps
- Formal parametric polymorphism
- A first order logic of effects
- Soundness of data refinement for a higher-order imperative language
- Game-theoretic analysis of call-by-value computation
- Operational reasoning for functions with local state
- Program Logics for Homogeneous Meta-programming
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Program logics for sequential higher-order control
- Completeness and Logical Full Abstraction in Modal Logics for Typed Mobile Processes
- Descriptive and Relative Completeness of Logics for Higher-Order Functions
- Logical Reasoning for Higher-Order Functions with Local State
- Title not available (Why is that?)
- Title not available (Why is that?)
- Even Simple Programs Are Hard To Analyze
- The Complexity of Finite Memory Programs with Recursion
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Hoare logic for Java in Isabelle/HOL
- From process logic to program logic
- A logic of object-oriented programs
- A logical analysis of aliasing in imperative higher-order functions
- Programming Languages and Systems
- Correspondence between ALGOL 60 and Church's Lambda-notation
- Title not available (Why is that?)
- The Mechanical Evaluation of Expressions
- Finitary PCF is not decidable
Cited In (12)
- Title not available (Why is that?)
- Small bisimulations for reasoning about higher-order imperative programs
- Symbolic execution proofs for higher order store programs
- A sound and complete Hoare logic for dynamically-typed, object-oriented programs
- A logical analysis of aliasing in imperative higher-order functions
- A logical analysis of aliasing in imperative higher-order functions
- Reverse Hoare logic
- Specification patterns and proofs for recursion through the store
- Title not available (Why is that?)
- Descriptive and Relative Completeness of Logics for Higher-Order Functions
- Crowfoot: A Verifier for Higher-Order Store Programs
- Nested Hoare Triples and Frame Rules for Higher-Order Store
Uses Software
This page was built for publication: An observationally complete program logic for imperative higher-order functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q387994)
