In computer science, algebraic semantics is a formal approach to programming language theory that uses algebraic methods for defining, specifying, and reasoning about the behavior of programs. It is a form of axiomatic semantics that provides a mathematical framework for analyzing programs through the use of algebraic structures and equational logic.

Algebraic semantics represents programs and data types as algebras—mathematical structures consisting of sets equipped with operations that satisfy certain equational laws. This approach enables rigorous formal verification of software by treating program properties as algebraic properties that can be proven through mathematical reasoning. A key advantage of algebraic semantics is its ability to separate the specification of what a program does from how it is implemented, supporting abstraction and modularity in software design.

The syntax of an algebraic specification is formulated in two steps: (1) defining a formal signature of data types and operation symbols, and (2) interpreting the signature through sets and functions.

The signature of an algebraic specification defines its formal syntax. The word "signature" is used like the concept of "key signature" in musical notation.

A signature consists of a set ${\displaystyle S}$ of data types, known as sorts, together with a family ${\displaystyle \Sigma }$ of sets, each set containing operation symbols (or simply symbols) that relate the sorts. We use ${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$ to denote the set of operation symbols relating the sorts ${\displaystyle s_{1},~s_{2},~...,~s_{n}\in S}$ to the sort ${\displaystyle s\in S}$.

For example, for the signature of integer stacks, we define two sorts, namely, ${\displaystyle int}$ and ${\displaystyle stack}$, and the following family of operation symbols:

where ${\displaystyle \Lambda }$ denotes the empty string.

An algebra ${\displaystyle A}$ interprets the sorts and operation symbols as sets and functions. Each sort ${\displaystyle s}$ is interpreted as a set ${\displaystyle A_{s}}$, which is called the carrier of ${\displaystyle A}$ of sort ${\displaystyle s}$, and each symbol ${\displaystyle \sigma }$ in ${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$ is mapped to a function ${\displaystyle \sigma _{A}:A_{s_{1}}\times A_{s_{2}}\times ~...\times ~A_{s_{n}}}$, which is called an operation of ${\displaystyle A}$.