scientific article
From MaRDI portal
Publication:3932278
zbMath0476.68010MaRDI QIDQ3932278
Publication date: 1981
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)
Related Items (27)
Logical relations and parametricity -- a Reynolds programme for category theory and programming languages ⋮ Constraint-based relational verification ⋮ The regular-language semantics of second-order idealized ALGOL ⋮ A categorical treatment of pre- and post-conditions ⋮ A note on undefined expression values in programming logics ⋮ On assertion-based encapsulation for object invariants and simulations ⋮ A calculus of refinements for program derivations ⋮ Full abstraction for the second order subset of an Algol-like language ⋮ Auxiliary variables in data refinement ⋮ Splitting atoms safely ⋮ Relational separation logic ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Monoidal indeterminates and categories of possible worlds ⋮ Do-it-yourself type theory ⋮ Semantical analysis of specification logic ⋮ An operational semantics of occam ⋮ Proof obligations for blocks and procedures ⋮ Continuations in possible-world semantics ⋮ Predicate transformers and higher-order programs ⋮ Algebraic proofs of consistency and completeness ⋮ A single complete rule for data refinement ⋮ The spirit of ghost code ⋮ Certified Reasoning with Infinity ⋮ Compositional Predicate Abstraction from Game Semantics ⋮ Monoidal Indeterminates and Categories of Possible Worlds ⋮ Semantics of interference control ⋮ Programs as proofs: A synopsis
This page was built for publication: