An observationally complete program logic for imperative higher-order functions
From MaRDI portal
Publication:387994
DOI10.1016/j.tcs.2013.11.003zbMath1358.68071OpenAlexW1661340274MaRDI QIDQ387994
Kohei Honda, Martin Berger, Nobuko Yoshida
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
completenesscharacteristic formulaeprogram logicobservational equivalencehigher-order functionimperative programming
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (5)
Crowfoot: A Verifier for Higher-Order Store Programs ⋮ Symbolic execution proofs for higher order store programs ⋮ Specification Patterns and Proofs for Recursion through the Store ⋮ Reverse Hoare Logic ⋮ Nested Hoare Triples and Frame Rules for Higher-Order Store
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Semantical analysis of specification logic
- 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
- Edinburgh LCF. A mechanized logic of computation
- On full abstraction for PCF: I, II and III
- Full abstraction for PCF
- Game-theoretic analysis of call-by-value computation
- Program Logics for Homogeneous Meta-programming
- Program Logics for Sequential Higher-Order Control
- Separation and information hiding
- 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
- Algebraic laws for nondeterminism and concurrency
- Ten Years of Hoare's Logic: A Survey—Part I
- Even Simple Programs Are Hard To Analyze
- The Complexity of Finite Memory Programs with Recursion
- Soundness and Completeness of an Axiom System for Program Verification
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Hoare logic for Java in Isabelle/HOL
- Equivalence in functional languages with effects
- Program verification through characteristic formulae
- Characteristic formulae for the verification of imperative programs
- From process logic to program logic
- Verification: Theory and Practice
- A logical analysis of aliasing in imperative higher-order functions
- Programming Languages and Systems
- Correspondence between ALGOL 60 and Church's Lambda-notation
- An axiomatic basis for computer programming
- The Mechanical Evaluation of Expressions
- Finitary PCF is not decidable
This page was built for publication: An observationally complete program logic for imperative higher-order functions
