I will present a style of operational semantics that we call omnisemantics, and whose judgments relate starting states to sets of outcomes rather than to individual outcomes.

A single derivation of these semantics for a particular starting state and program describes all possible nondeterministic executions (hence the name omni), whereas in traditional small-step and big-step semantics, each derivation only talks about one single execution.

This restructuring allows for straightforward modeling of both nondeterminism and undefined behavior as commonly encountered in sequential functional and imperative programs. Specifically, omnisemantics inherently assert safety, i.e. they guarantee that none of the execution branches gets stuck, while traditional semantics need either a separate judgment or additional error markers to specify safety in the presence of nondeterminism.

Omnisemantics can be understood as an inductively defined weakest-precondition semantics (or more generally, predicate-transformer semantics) that does not involve invariants for loops and recursion but instead uses unrolling rules like in traditional small-step and big-step semantics.

Omnisemantics were previously described (under different names) in association with several projects, but we believe the technique has been underappreciated and deserves a well-motivated presentation of its benefits.

We also explore several novel aspects associated with these semantics, in particular their use in type-safety proofs for lambda calculi, partial-correctness reasoning, and forward proofs of compiler correctness for terminating but potentially nondeterministic programs being compiled to nondeterministic target languages.

All results have been formalized in Coq, and omnisemantics serve as the semantic backbone throughout our verified software/hardware stack that we’re developing in the PLV group at MIT.