> For the complete documentation index, see [llms.txt](https://isubasinghe.gitbook.io/isithas-wiki/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://isubasinghe.gitbook.io/isithas-wiki/computer_science/programming_language_theory/semantics.md).

# semantics

## Basic idea

Formal meaning of programs. Three classical styles: *operational* (how it runs, step-by-step), *denotational* (what mathematical object it denotes), *axiomatic* (which logical properties hold).

## Key formulas

* Small-step: $e \to e'$
* Big-step: $e \Downarrow v$
* Denotational: $\llbracket e \rrbracket : \text{Env} \to \text{Val}$
* Hoare triple (axiomatic): ${P}\ C\ {Q}$
* Induction reasons about least fixed points; coinduction reasons about greatest fixed points.
* Interaction trees represent effectful, recursive computations coinductively.
* Scott-continuous functions give recursive programs least fixed-point denotations.
* Labelled transition systems support trace semantics and strong or weak bisimulation.
* Strong normalization rules out every infinite reduction sequence for well-typed terms in calculi such as STLC and System F.