INCLUSION CRITERIA
An entry belongs in this subdivision if and only if it is a logic or calculus whose subject is the meaning or behavior of computation—how programs execute, what they denote, or how processes interact.
Required: At least one of the following:
- A semantics of programs (operational, denotational, axiomatic) or domain theory
- A process, concurrency, or mobility calculus with a defined reduction or bisimulation
- A rewriting, equational, or constraint calculus modeling computation
Not sufficient: A logic for proving program correctness (Verification). A type system as such (Type). A logic for natural-language meaning (Semantics).
Boundary: Denotational semantics and domain theory are cross-listed with Metatheory/Categorical. Correctness logics (Hoare, separation) belong in Verification. Computability logic here is Japaridze's game-semantic calculus; the recursion-theoretic notion of computability is in Metatheory/Computability.