Denotational semantics

denotationalfully abstractHistory of denotational semanticscompositionalitycompositionality of programming languagesconcurrencydenotational modelsdenotational semantics of concurrencyfull abstraction
In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called denotations) that describe the meanings of expressions from the languages.wikipedia
132 Related Articles

Operational semantics

operationalnatural semanticsOperationally
Other approaches provide formal semantics of programming languages including axiomatic semantics and operational semantics.
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics).

Christopher Strachey

ChristopherChristopher Stratchey
Denotational semantics originated in the work of Christopher Strachey and Dana Scott published in the early 1970s.
He was one of the founders of denotational semantics, and a pioneer in programming language design.

Domain theory

domainsdomaindomain theoretic
Broadly speaking, denotational semantics is concerned with finding mathematical objects called domains that represent what programs do. To give meanings to recursively defined programs, Scott proposed working with continuous functions between domains, specifically complete partial orders.
The field has major applications in computer science, where it is used to specify denotational semantics, especially for functional programming languages.

Semantics (computer science)

semanticsformal semantics of programming languagesformal semantics
Other approaches provide formal semantics of programming languages including axiomatic semantics and operational semantics.

Complete partial order

directed complete partial ordercpodirected-complete partial order
To give meanings to recursively defined programs, Scott proposed working with continuous functions between domains, specifically complete partial orders.
Complete partial orders play a central role in theoretical computer science, in denotational semantics and domain theory.

Axiomatic semantics

axioms
Other approaches provide formal semantics of programming languages including axiomatic semantics and operational semantics.

Principle of compositionality

compositionalitycompositionalcompositional semantics
An important tenet of denotational semantics is that semantics should be compositional: the denotation of a program phrase should be built out of the denotations of its subphrases.
The principle of compositionality also exists in a similar form in the compositionality of programming languages.

Dana Scott

Dana S. ScottScottD. S. Scott
Denotational semantics originated in the work of Christopher Strachey and Dana Scott published in the early 1970s.
Together, their work constitutes the Scott–Strachey approach to denotational semantics; it constitutes one of the pieces of work in theoretical computer science and can perhaps be regarded as founding one of the schools of computer science.

Power domains

Powerdomain
The concept of power domains has been developed to give a denotational semantics to non-deterministic sequential programs.
In denotational semantics and domain theory, power domains are domains of nondeterministic and concurrent computations.

Scott continuity

Scott topologyScott-continuouscontinuous functions
To give meanings to recursively defined programs, Scott proposed working with continuous functions between domains, specifically complete partial orders.
Scott-continuous functions show up in the study of models for lambda calculi and the denotational semantics of computer programs.

Denotational semantics of the Actor model

Clinger's modeldenotational modelsdenotational semantics
Examples include Will Clinger's work with the actor model; Glynn Winskel's work with event structures and petri nets; and the work by Francez, Hoare, Lehmann, and de Roever (1979) on trace semantics for CSP.
The denotational semantics of the Actor model is the subject of denotational domain theory for Actors.

Unbounded nondeterminism

fairnessbounded nondeterminismfair
There are difficulties with fairness and unboundedness in domain-theoretic models of non-determinism.
Unbounded nondeterminism became an important issue in the development of the denotational semantics of concurrency, and later became part of research into the theoretical concept of hypercomputation.

Communicating sequential processes

CSPCommunicating Sequential Processes (CSP)channel
Denotational semantics have been developed for modern programming languages that use capabilities like concurrency and exceptions, e.g., Concurrent ML, CSP, and Haskell.
The theory of CSP includes mutually consistent denotational semantics, algebraic semantics, and operational semantics.

Partial function

total functionpartialtotal
For example, programs (or program phrases) might be represented by partial functions or by games between the environment and the system.
In denotational semantics a partial function is considered as returning the bottom element when it is undefined.

Concurrency (computer science)

concurrencyconcurrentconcurrently
Many researchers have argued that the domain-theoretic models given above do not suffice for the more general case of concurrent computation.
For example, Lee and Sangiovanni-Vincentelli have demonstrated that a so-called "tagged-signal" model can be used to provide a common framework for defining the denotational semantics of a variety of different models of concurrency, while Nielsen, Sassone, and Winskel have demonstrated that category theory can be used to provide a similar unified understanding of different models.

Fixed-point theorem

fixed point theoremfixed point theoryfixed-point theory
So by a fixed-point theorem (specifically Bourbaki–Witt theorem), there exists a fixed point for this iterative process.
In denotational semantics of programming languages, a special case of the Knaster–Tarski theorem is used to establish the semantics of recursive definitions.

Linear logic

Intuitionistic linear logicmultimap
Following the development of programming languages based on linear logic, denotational semantics have been given to languages for linear usage (see e.g. proof nets, coherence spaces) and also polynomial time complexity.
In terms of simple denotational models, linear logic may be seen as refining the interpretation of intuitionistic logic by replacing cartesian (closed) categories by symmetric monoidal (closed) categories, or the interpretation of classical logic by replacing Boolean algebras by C*-algebras.

Actor model

actorsactorActor programming
For denotational semantics in more intensional models, such as the actor model and process calculi, there are different notions of equivalence within each model, and so the concepts of adequacy and of full abstraction are a matter of debate, and harder to pin down.

Iterated function

iterationiteratesiterate
In computer science, iterated functions occur as a special case of recursive functions, which in turn anchor the study of such broad topics as lambda calculus, or narrower ones, such as the denotational semantics of computer programs.

Programming Computable Functions

PCFLCF languageProgramming language for Computable Functions
The problem of full abstraction for the sequential programming language PCF was, for a long time, a big open question in denotational semantics.
A fully abstract model for PCF was first given by Milner (1977).

Lambda calculus

beta reductionλ-calculusuntyped lambda calculus
For another example: the type of denotations of the untyped lambda calculus is
This work also formed the basis for the denotational semantics of programming languages.

Formal verification

program verificationverificationautomated verification
Within computer science, there are connections with abstract interpretation, program verification, and model checking.
Examples of mathematical objects often used to model systems are: finite state machines, labelled transition systems, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic.

Game semantics

game semantics for first-order logicgame theoretic semanticsGame-theoretical semantics
This open question was mostly resolved in the 1990s with the development of game semantics and also with techniques involving logical relations.
Using game semantics, the authors mentioned above have solved the long-standing problem of defining a fully abstract model for the programming language PCF.

Logical relations

This open question was mostly resolved in the 1990s with the development of game semantics and also with techniques involving logical relations.
Logical relations are a proof method employed in programming language semantics to show that two denotational semantics are equivalent.

Computer science

computer scientistcomputer sciencescomputer scientists
In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called denotations) that describe the meanings of expressions from the languages.