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.

Pages

• codegen
• computations
• optimisations
• parsers
• semantics
• types

Siblings

• ai
• compression
• computer algebra
• data structures
• distributed systems
• formal verification
• Operating Systems
• search
• theoretical