Online Encyclopedia Search Tool

Your Online Encyclopedia


Online Encylopedia and Dictionary Research Site

Online Encyclopedia Free Search Online Encyclopedia Search    Online Encyclopedia Browse    welcome to our free dictionary for your research of every kind

Online Encyclopedia

Formal semantics of programming languages

(Redirected from Formal semantics)

In theoretical computer science formal semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation.

The formal semantics of a language is given by a mathematical model to represent the possible computations described by the language.

There are many approaches to providing a formal semantics for programming languages. The three main classes of approach are:

but additionally there are awkward cases that do not obviously fit into the above classes, such as:

  • Action semantics, which seems to be a kind of hybrid of axiomatic and operational semantics;
  • Categorical semantics (also called Functorial semantics ), which is most easily understood as an algebraic semantics (and so is an axiomatic semantics), but which can also be understood as a kind of denotational semantics, and indeed familiarity with category theory is today a requirement for understanding most work in denotational semantics;
  • Game semantics was proposed as a kind of denotational semantics, but it has a dynamical aspect that allows it to be understood as a kind of operational semantics.

Different formal semantics may be linked through abstractions within the theory of abstract interpretation.

The field of formal semantics also studies the relations between different models, the relations between different approaches to meaning, and the relation between computation and the underlying mathematical structures, from fields such as logic, set theory, model theory, category theory, etc.

It has close links with other areas of computer science such as Programming language design , Type theory, Compilers and Interpreters, Program verification and Model checking.

External link

Last updated: 10-24-2004 05:10:45