An observationally complete program logic for imperative higher-order functions
From MaRDI portal
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
Cites work
- scientific article; zbMATH DE number 439891 (Why is no real title available?)
- scientific article; zbMATH DE number 3858385 (Why is no real title available?)
- scientific article; zbMATH DE number 3890703 (Why is no real title available?)
- scientific article; zbMATH DE number 5605107 (Why is no real title available?)
- scientific article; zbMATH DE number 3936465 (Why is no real title available?)
- scientific article; zbMATH DE number 3697087 (Why is no real title available?)
- scientific article; zbMATH DE number 3716792 (Why is no real title available?)
- scientific article; zbMATH DE number 3748394 (Why is no real title available?)
- scientific article; zbMATH DE number 512792 (Why is no real title available?)
- scientific article; zbMATH DE number 605917 (Why is no real title available?)
- scientific article; zbMATH DE number 1556014 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- scientific article; zbMATH DE number 3304881 (Why is no real title available?)
- A first order logic of effects
- A logic of object-oriented programs
- A logical analysis of aliasing in imperative higher-order functions
- A sound and relatively* complete Hoare-logic for a language with higher type procedures
- Algebraic laws for nondeterminism and concurrency
- An axiomatic basis for computer programming
- Axiomatic approach to side effects and general jumps
- Characteristic formulae for the verification of imperative programs
- Completeness and Logical Full Abstraction in Modal Logics for Typed Mobile Processes
- Correspondence between ALGOL 60 and Church's Lambda-notation
- Descriptive and Relative Completeness of Logics for Higher-Order Functions
- Edinburgh LCF. A mechanized logic of computation
- Equivalence in functional languages with effects
- Even Simple Programs Are Hard To Analyze
- Finitary PCF is not decidable
- Formal parametric polymorphism
- From process logic to program logic
- Full abstraction for PCF
- Game-theoretic analysis of call-by-value computation
- Hoare logic for Java in Isabelle/HOL
- Logical Reasoning for Higher-Order Functions with Local State
- On full abstraction for PCF: I, II and III
- Operational reasoning for functions with local state
- Program Logics for Homogeneous Meta-programming
- Program logics for sequential higher-order control
- Program verification through characteristic formulae
- Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
- Programming Languages and Systems
- Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
- Semantical analysis of specification logic
- Separation and information hiding
- Sound and complete Hoare-like calculi based on copy rules
- Soundness and Completeness of an Axiom System for Program Verification
- Soundness of data refinement for a higher-order imperative language
- Ten Years of Hoare's Logic: A Survey—Part I
- The Complexity of Finite Memory Programs with Recursion
- The Mechanical Evaluation of Expressions
- Types and programing languages
Cited in
(12)- Nested Hoare Triples and Frame Rules for Higher-Order Store
- scientific article; zbMATH DE number 3997138 (Why is no real title available?)
- 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
- scientific article; zbMATH DE number 6991660 (Why is no real title available?)
- Descriptive and Relative Completeness of Logics for Higher-Order Functions
- Crowfoot: A Verifier for Higher-Order Store Programs
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)
