> 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.md).

# programming\_language\_theory

## Basic idea

Formal study of how programming languages are described, type-checked, compiled, and given meaning. Spans syntax (parsers), semantics, type systems, optimisations, and code generation.

## Key formulas

* Hoare triple: ${P}\ C\ {Q}$
* Typing judgement: $\Gamma \vdash e : \tau$
* Operational step: $e \to e'$
* Curry-Howard: types ≅ propositions, programs ≅ proofs.