What are different ways to provide a semantics to a language?

Suppose you have 1. a grammar for terms of a language; 2. type-assignment rules, 3. a set of reduction rules. You want to prove that your language is adequate for mathematical reasoning. If I understand correctly, the right way to do it is to develop a semantics for it, and then prove certain desirable properties such as soundness and consistency.

I've seen different approaches to this. Usually, a model in set theory is involved. But I believe that is not the only way to do it. Wouldn't, for example, an interpreter for that language on the untyped λ-calculus count as a semantics? So, my question is: what are the different ways to provide a semantics to language?

There are many possible approaches. Here's a few "classic" styles.

• Operational semantics (e.g. small step / reduction, or big step)

• Denotational semantics (e.g. domain-theoretic, or category-theoretic)

• Axiomatic semantics (e.g. hoare logic)

You can also define the semantics of a language through a translation to another language (already having its semantics). CPS transforms could also be mentioned here.

Also note that many languages admit several distinct semantics. Lazy & eager semantics of functional programs are possible, for instance. Prolog also has many different semantics (I recall someone stating "there's no such a thing as THE semantics of Prolog").

Further, concurrent languages like CCS or $\pi$-calculus have a LTS semantics. Game semantics is also used sometimes (but I don't know much about it).

I'm pretty sure there are many other kinds of semantics. I'd be surprised if in the future someone does not invent a new kind of semantics.

StackExchange Computer Science Q#103333, answer score: 5