In computer science, denotational semantics is an approach to formalizing the semantics of computer systems by constructing mathematical objects (called denotations or meanings) which express the semantics of these systems. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and operational semantics. The denotational approach to semantics was originally developed to deal only with systems defined by a single computer program. Later the field broadened to include systems composed of more than one program, such as those found in networking and concurrent systems. Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. ... In the main, semantics (from the Greek and in greek letters σημαντικός or in latin letters semantikós, or significant meaning, derived from sema, sign) is the study of meaning, in some sense of that term. ... A computer system is an automated data-processing system that uses a programmable electronic device to store, retrieve, and process data. ... 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. ... Axiomatic Semantics is an approach based on mathematical logic to proving the correctness of computer programs. ... In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way (See formal semantics of programming languages). ... A computer program or software program (usually abbreviated to a program) is a step-by-step list of instructions written for a particular computer architecture in a particular computer programming language. ... A computer network is a system for communication between computers. ... Concurrent systems are an area of study in computer science, where concurrency or parallelism is important. ...

Denotational semantics originated in the work of Christopher Strachey and Dana Scott in the 1960s. As originally developed by Strachey and Scott, denotational semantics interpreted the denotation (meaning) of a computer program as a function that mapped input into output. Later, this proved to be too limiting to allow the definition of denotations (meanings) for programs that included elements such as recursively defined functions and data structures. Seeking to address these difficulties, Scott introduced a generalized approach to denotational semantics, based on domains (Abramsky and Jung 1994). Later researchers introduced approaches based on power domains, in an effort to address difficulties with the semantics of concurrent systems (Clinger 1981). Christopher Strachey (1916–1975) was a British computer scientist. ... This article needs cleanup. ... The 1960s decade refers to the years from 1960 to 1969, inclusive. ... Partial plot of a function f. ... A Sierpinski triangle —a confined recursion of triangles to form a geometric lattice. ... Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. ... In denotational semantics power domains are used to construct denotations of programs. ... Wikiquote has a collection of quotations related to: Edsger Dijkstra In computer science, concurrency is a property of systems which consist of computations that execute overlapped in time, and which may permit the sharing of common resources between those overlapped computations. ...

Fixed point semantics

The denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do. The theory makes use of a computational mathematical domains. Examples of such computational domains are partial functions and Actor event diagram scenarios. Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. ... In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ...

The relationship x≤y means that x can computationally evolve to y. If the denotations are partial functions, for example, f≤g may mean that f agrees with g on all values for which f is defined. If the denotations are Actor event diagram scenarios, x≤y means that a system which satisfies x can evolve into a system which satisfies y. In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ...

Computational domains have the following properties:

1. Bottom exists. The domain has a least element denoted by ⊥ such that for every element x in the domain ⊥≤x.
2. Limits exist. As computation continues, the denotations should become better and have a limit so if we have ∀i∈ω x_i≤x_i+1 then the least upper bound ∨_i∈ω x_i should exist. The property just stated is called ω-completeness.
3. Finite elements are countable. An element x is finite (also called isolated in the domain literature) if and only if whenever A is directed, ∨A exists and x≤∨A, there exists a∈A with x≤a. In other words, x is finite if one must go through x in order to get up to or above x via the limit process.
4. Every element is the least upper bound of a countable increasing sequence of finite elements. Intuitively this means that every element can be reached by a computational process in which each progression is finite.
5. The domain is downward closed.

The mathematical denotation denoted by a system S is found by solving by constructing increasingly better approximations from an initial empty denotation called ⊥_S using some denotation approximating function progression_S to construct a denotation (meaning ) for S as follows [Hewitt 2006b]: In mathematics, the supremum of an ordered set S is the least element (not necessarily in S) which is greater than or equal to each element of S. Consequently, it is also referred to as the least upper bound. ... In mathematics, a directed set is a set A together with a binary relation ≤ having the following properties: a ≤ a for all a in A (reflexivity) if a ≤ b and b ≤ c, then a ≤ c (transitivity) for any two a and b in A, there exists a c in A...

Denote_S ≡ ∨_i∈ω progression_Sⁱ(⊥_S).

It would be expected that progression_S would be monotone, i.e., if x≤y then progression_S(x)≤progression_S(y). More generally, we would expect that

If ∀i∈ω x_i≤x_i+1, then progression_S(∨_i∈ω x_i) = ∨_i∈ω progression_S(x_i)

This last stated property of progression_S is called ω-continuity.

A central question of denotational semantics is to characterize when it is possible to create denotations (meanings) in according to the equation for Denote_S. A fundamental theorem of computational domain theory is that if progression_S is ω-continuous then Denote_S will exist.

It follows from the ω-continuity of progression_S that

progression_S(Denote_S) = Denote_S

The above equation motivates the terminology that Denote_S is a fixed point of progression_S.

Furthermore this fixed point is least among all fixed points of progression_S.

The denotational semantics of functional programs provides an example of fixed point semantics as shown in the next section.

Example of factorial function

Consider the factorial function which is defined on all non-negative numbers as follows:

factorial ≡ λ(n)if (n==0)then 1 else n*factorial(n-1)

The graph of factorial is the set of all ordered pairs for which factorial is defined with the first element of an ordered pair being the argument and the second element being the value, e.g.,

graph(factorial) = {<n, factorial(n)>|n∈ω} = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}

The denotation (meaning) Denote_factorial for the factorial program is constructed as follows:

Denote_factorial = graph(factorial) = ∪_i∈ω progression_factorialⁱ({})

where

progression_factorial(g) ≡ λ(n)if (n==0)then 1 else n*g(n-1)

Note: progression_factorial is a fix point operator (see definition in section above) whose least fixed point is Denote_factorial, i.e.,

Denote_factorial = progression_factorial(Denote_factorial)

Also progression_factorial is ω-continuous (see definition in section above).

Derivation of Scott Continuity from Actor Semantics

The Actor model provides a foundation for deriving Dana Scott's denotational semantics of functions (as illustrated in the previous section above for factorial) as demonstrated first by a theorem of Carl Hewitt and Henry Baker [1977]: In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ... This article needs cleanup. ... Carl E. Hewitt is an Associate Professor (Emeritus) in the Electrical Engineering and Computer Science department at the Massachusetts Institute of Technology (MIT). ... Henry Baker is the name of a computer scientist who has made contributions in such areas as Garbage collection and the Actor model. ...

If an Actor f behaves like a mathematical function, then progression_f is a Scott continuous functional whose least fixed point is A monotone function f : P → Q between posets P and Q is Scott-continuous if, for every directed set D that has a supremum sup D in P, the set {fx | x in D} has the supremum f(sup D) in Q. Stated differently, a Scott-continuous function is one...

graph(f) = ∪_i∈ω progression_fⁱ({})

where

progression_f(G)≡{<x, y>|<x, y>∈graph(f) and immediate-descendants_f(<x, y>)⊆G}

The paper by Hewitt and Baker contained a small bug in the definition of immediate-descendants_f that was corrected in Will Clinger [1981].

Full abstraction

The concept of full abstraction is concerned with whether the denotational semantics for a program is an exact match for its operational semantics. Key properties of full abstraction are:

1. Abstractness: The denotational semantics must be formalised using mathematical structures that are independent of the representation and operational semantics of the programming language;
2. Soundness: All observably distinct programs have distinct denotations;
3. Completeness: Any two programs with distinct denotations must be observably distinct.

Additional desirable properties we may wish to hold between operational and denotational semantics are: Two terms M and N are observationally equivalent if for all contexts C[] where C[M] is a valid term, C[N] is also a valid term with the same value. ...

1. Constructivity: The semantic model should be constructive in the sense that it should only include elements that can be intuitively constructed. One way of formalizing this is that every element must be the limit of a directed set of finite elements.
2. Progressivity: For each system S, there is a progression_S function for the semantics such that the denotation (meaning ) of a system S is ∨_i∈ωprogression_Sⁱ(⊥_S) where ⊥_S is the initial configuration of s.
3. Full completeness: Every morphism of the semantic model should be the denotation of a program.

A long-standing issue in denotational semantics was full abstraction in the presence of inductive datatypes, particularly the type of natural numbers, as a type admitting usage as a method of recursion. A traditional interpretation of this question was as semantics for the system PCF. The success achieved by game semantics in providing fully abstract models in the 1990s for PCF led to a fundamental change in the way that work on denotational semantics was done. In computer programming languages, a recursive type is a data type for values that may contain other values of the same type. ... Natural number can mean either a positive integer (1, 2, 3, 4, ...) or a non-negative integer (0, 1, 2, 3, 4, ...). Natural numbers have two main purposes: they can be used for counting (there are 3 apples on the table), or they can be used for ordering (this is... A Sierpinski triangle —a confined recursion of triangles to form a geometric lattice. ... PCF or Programming language for Computable Functions is a typed functional language introduced by Gordon Plotkin in 1977. ... Game semantics (German: dialogische Logik) is an approach to the semantics of logic that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player. ... The 1990s decade refers to the years from 1990 to 1999, inclusive. ...

Compositionality in programming languages

See main article principle of compositionality In mathematics, semantics, and philosophy of language, the Principle of Compositionality is the principle that the meaning of a complex expression is determined by the meanings of its constituent expressions and the rules used to combine them. ...

An important aspect of denotational semantics of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts. For example consider the expression "<expression₁> + <expression₂>". Compositionality in this case is to provide a meaning for "<expression₁> + <expression₂>" in terms of the meanings of <expression₁> and <expression₂>.

Environments

The Actor model provides a modern and very general way the compositionality of programs can be analyzed. In this analysis, programs are Actors that are sent Eval messages with the address of an environment Actor so that programs inherit their denotational semantics from the denotational semantics of the Actor model (an idea published in Hewitt [2006a]). The environment holds the bindings of identifiers. When an environment is sent a Lookup message with the address of an identifier x, it returns the latest (lexical) binding of x. In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ... The denotational semantics of the Actor model is the subject of mathematical models for Actors based on domain theory. ...

As an example of how this works consider the lambda expression <L> below which implements a tree data structure when supplied with parameters for a leftSubTree and rightSubTree. When such a tree is given a parameter message "getLeft", it returns leftSubTree and likewise when given the message "getRight" it returns rightSubTree.

 λ(leftSubTree, rightSubTree) λ(message) if (message == "getLeft") then leftSubTree else if (message == "getRight") then rightSubTree 

Consider what happens when an expression of the form "(<L> 1 2)" is sent an Eval message with environment E. One semantics for application expressions such as this one is the following: <L>, 1 and 2 are all sent Eval messages with environment E. The integers 1 and 2 immediately reply to the Eval message with themselves.

However <L> responds to the Eval message by creating a closure Actor (process) C that has an address (called body) for <L> an address (called environment) for E. The Actor "(<L> 1 2)" then sends C the message [1 2]. In programming languages, a closure is a function that refers to free variables in its lexical context. ...

When C receives the message [1 2], it creates a new environment Actor F which behaves as follows:

1. When it receives a Lookup message for the identifier leftSubTree it responds with 1
2. When it receives a Lookup message for the identifier rightSubTree it responds with 2
3. When it receives a Lookup message for any other identifier, it forwards the Lookup message to E.

The Actor (process) C then sends an Eval message with environment F to the following actor (process):

 λ(message) if (message == "getLeft") then leftSubTree else if (message == "getRight") then rightSubTree 

Arithmetic expressions

For another example consider the Actor for the expression "<expression₁> + <expression₂>" which has addresses for two other actors (processes) <expression₁> and <expression₂>). When the composite expression Actor (process) receives an Eval message with addresses for an environment Actor E and a customer C, it sends Eval messages to expression₁ and <expression₂ with environment E and customer a new Actor (process) C₀. When C₀ has received back two values N₁ and N₂, it sends C the value N₁ + N₂. In this way, the denotational semantics for process calculi and the Actor model provide a denotational semantics for "<expression₁> + <expression₂>" in terms of the semantics for <expression₁> and <expression₂>. The process calculi (or process algebras) are a diverse family of related approaches to formally modelling concurrent systems. ... In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ...

Delayed evaluation

Providing a denotational compositional semantics for delayed evaluation provides a challenge for denotational semantics. The problem with classical approaches for compositional denotational semantics in dealing with expressions of form "delay <Expression>" has been how to formalize the semantics of the evaluation of <Expression>.

The denotational semantics of process calculi and the Actor model provides a perfectly reasonable account: The process calculi (or process algebras) are a diverse family of related approaches to formally modelling concurrent systems. ... In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ...

The delay expression responds to an <Eval> message with environment E by creating a closure Actor C that has an address (called body) for <Expression> an address (called environment) for E.

When C receives a message M with Customer₀, it creates a new Actor (process) Customer₁ and sends <Expression> an Eval message with environment E and the address of Customer₁.

When Customer₁ receives a value V, it sends V the message M with Customer₀.

Other programming language constructs can be provided compositional semantics in similar ways. In programming languages, a closure is a function that refers to free variables in its lexical context. ...

The denotational compositional semantics presented above is very general and can be used for functional, imperative, concurrent, logic, etc. programs Functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions. ... In computer science, imperative programming, as opposed to declarative programming, is a programming paradigm that describes computation in terms of a program state and statements that change the program state. ... Concurrent programming languages are programming languages that use language constructs for concurrency. ... Logic programming (sometimes called logical programming) is programming that makes use of pattern-directed invocation of procedures from assertions and goals. ...

Denotational semantics of concurrency

Two principle approaches to denotational semantics of concurrency are those based on the process calculi and the Actor model (see denotational semantics of the Actor model). Extending denotational semantics to concurrency proved challenging (see unbounded nondeterminism). The process calculi (or process algebras) are a diverse family of related approaches to formally modelling concurrent systems. ... In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ... The denotational semantics of the Actor model is the subject of mathematical models for Actors based on domain theory. ... In computer science, unbounded nondeterminism (sometimes called unbounded indeterminacy) is a property of concurrency by which the amount of delay in servicing a request can become unbounded as a result of arbitration of contention for shared resources while still guaranteeing that the request will eventually be serviced. ...

Early history of denotational semantics

As mentioned earlier, the field was initially developed by Christopher Strachey and Dana Scott in the 1960s and then Joe Stoy in the 1970s at the Programming Research Group, part of the Oxford University Computing Laboratory. Christopher Strachey (1916–1975) was a British computer scientist. ... This article needs cleanup. ... The 1960s decade refers to the years from 1960 to 1969, inclusive. ... Joe Stoy is a British computer scientist, although he originally studied physics at Oxford University. ... The 1970s decade refers to the years from 1970 to 1979, inclusive. ... The Programming Research Group is based at Oxford Universitys Computing Laboratory. ... The Oxford University Computing Laboratory (OUCL) is the computer science department at Oxford University in England. ...

Montague grammar is a form of denotational semantics for idealized fragments of English. Montague grammar is an approach to natural language semantics, based on formal logic, especially lambda calculus and set theory. ... The English language is a West Germanic language that originates in England. ...

According to Clinger [1981],

Plotkin's original power domain construction was simplified in [Smyth 1978] which remains the standard introduction to the subject. A number of nondeterministic programming languages have now been given power domain semantics. Of these the semantics of [Francez, Hoare, Lehmann, and de Roever 1979] had the most influence over the development of the denotational model in Clinger's dissertation.

The denotational semantics in Clinger's dissertation is probably the first power domain semantics for languages with true concurrency, but it is not the first power domain semantics for a language with unbounded nondeterminism. [Back 1980] has given a power domain semantics for a language with unboundedly nondeterministic assignment as a primitive operation. Three differences between Back's work and the Actor denotation semantics in Clinger's dissertation stand out:

1. The source of nondeterminism in Back's paper is basic assignment statements whereas in the Actor model it is message latency.
2. Back's paper treats nondeterministic sequential programming languages whereas the Actor model is concerned with concurrent programming languages.
3. The power domain in Back's paper apparently is constructed from a complete underlying domain. This third difference is not entirely clear because Back's power domain construction appears to be nonstandard.

A similarity between Back's work the Actor denotational semantics in Clinger's dissertation is that Back found it necessary to build the power domain out of execution sequences instead of single states: the Actor power domain is built out of Actor event diagrams, which are generalizations of execution sequences.

Gordon D. Plotkin FRS is a computer scientist. ... Sir Charles Antony Richard Hoare (Tony Hoare or C.A.R. Hoare, born January 11, 1934) is a British computer scientist, probably best known for the development of Quicksort, the worlds most widely used sorting algorithm, in 1960. ...

Connections to other areas of computer science

Some work in denotation semantics has interpreted types as domains in the sense of domain theory which can be seen a branch of model theory. and has many connections with type theory and category theory. Within computer science, there are connections with abstract interpretation, program verification and functional programming, see for instance monads in functional programming. In particular, denotational semantics has used the concept of continuations to express control flow in sequential programming in terms of functional programming semantics. Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. ... In mathematics, model theory is the study of the representation of mathematical concepts in terms of set theory, or the study of the models which underlie mathematical systems. ... At the broadest level, type theory is the branch of mathematics and logic that concerns itself with classifying entities into collections called types. ... Category theory is a mathematical theory that deals in an abstract way with mathematical structures and relationships between them. ... Abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. ... Program verification is the process of formally proving that a computer program does exactly what is stated in the program specification it was written to realize. ... Functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions. ... This article contains information that has not been verified and thus might not be reliable. ... In computing, a continuation is a representation of the execution state of a program (for example, the register contents and call stack) at a certain point in time. ... Functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions. ...

References

• ^- S. Abramsky and A. Jung: Domain theory. In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, vol. III. Oxford University Press, 1994. (ISBN 019853762X)
• Irene Greif. Semantics of Communicating Parallel Professes MIT EECS Doctoral Dissertation. August 1975.
• Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
• Gordon Plotkin. A powerdomain construction SIAM Journal of Computing September 1976.
• Edsger Dijkstra. A Discipline of Programming Prentice Hall. 1976.
• Krzysztof R. Apt, J. W. de Bakker. Exercises in Denotational Semantics MFCS 1976: 1-11
• J. W. de Bakker. Least Fixed Points Revisited Theor. Comput. Sci. 2(2): 155-181 (1976)
• Carl Hewitt and Henry Baker Actors and Continuous Functionals Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1–5, 1977.
• Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
• Michael Smyth. Power domains Journal of Computer and System Sciences. 1978.
• C.A.R. Hoare. Communicating Sequential Processes CACM. August, 1978.
• George Milne and Robin Milner. Concurrent processes and their syntax JACM. April, 1979.
• Nissim Francez, C.A.R. Hoare, Daniel Lehmann, and Willem-Paul de Roever. Semantics of nondeterminism, concurrency, and communication Journal of Computer and System Sciences. December 1979.
• Nancy Lynch and Michael Fischer. On describing the behavior of distributed systems in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Jerald Schwartz Denotational semantics of parallelism in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• William Wadge. An extensional treatment of dataflow deadlock Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Ralph-Johan Back. Semantics of Unbounded Nondeterminism ICALP 1980.
• David Park. On the semantics of fair parallelism Proceedings of the Winter School on Formal Software Specification. Springer-Verlag. 1980.
• ^- Will Clinger, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation, June 1981.
• Lloyd Allison, A Practical Introduction to Denotational Semantics Cambridge University Press. 1987.
• P. America, J. de Bakker, J. N. Kok and J. Rutten. Denotational semantics of a parallel object-oriented language Information and Computation, 83(2): 152 - 205 (1989)
• David A. Schmidt, The Structure of Typed Programming Languages. MIT Press, Cambridge, Massachusetts, 1994. ISBN 026269171X.
• M. Korff True concurrency semantics for single pushout graph transformations with applications to actor systems Working papers of the Int. Workshop on Information Systems - Correctness and Reusability. World Scientific. 1995.
• M. Korff and L. Ribeiro Concurrent derivations as single pushout graph grammar processes Proceedings of the Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation. ENTCS Vol 2, Elsevier. 1995.
• Thati, Prasanna, Carolyn Talcott, and Gul Agha. Techniques for Executing and Reasoning About Specification Diagrams International Conference on Algebraic Methodology and Software Technology (AMAST), 2004.
• J. C. M. Baeten. A brief history of process algebra Theoretical Computer Science. 2005.
• J.C.M. Baeten, T. Basten, and M.A. Reniers. Algebra of Communicating Processes Cambridge University Press. 2005.
• He Jifeng and C.A.R. Hoare. Linking Theories of Concurrency United Nations University International Institute for Software Technology UNU-IIST Report No. 328. July, 2005.
• Luca Aceto and Andrew D. Gordon (editors). Algebraic Process Calculi: The First Twenty Five Years and Beyond Process Algebra. Bertinoro, Forl`ı, Italy, August 1–5, 2005.
• Bill Roscoe. The Theory and Practice of Concurrency Prentice-Hall. 2005.
• Carl Hewitt (2006a). The repeated demise of logic programming and why it will be reincarnated What Went Wrong and Why: Lessons from AI Research and Applications. Technical Report SS-06-08. AAAI Press. March 2006.
• Carl Hewitt (2006b) What is Commitment? Physical, Organizational, and Social COIN@AAMAS. 2006.

Joe Stoy is a British computer scientist, although he originally studied physics at Oxford University. ... MIT Press Books The MIT Press is a university publisher affiliated with the Massachusetts Institute of Technology (MIT) in Cambridge, Massachusetts. ... Portrait of Edsger Dijkstra (courtesy Brian Randell) Prof Dr Edsger Wybe Dijkstra (Rotterdam, May 11, 1930 – Nuenen, August 6, 2002) was a Dutch computer scientist. ... Pearson can mean Pearson PLC the media conglomerate. ... Carl E. Hewitt is an Associate Professor (Emeritus) in the Electrical Engineering and Computer Science department at the Massachusetts Institute of Technology (MIT). ... Henry Baker is the name of a computer scientist who has made contributions in such areas as Garbage collection and the Actor model. ... Henry Baker is the name of a computer scientist who has made contributions in such areas as Garbage collection and the Actor model. ... Sir Charles Antony Richard Hoare (Tony Hoare or C.A.R. Hoare, born January 11, 1934) is a British computer scientist, probably best known for the development of Quicksort, the worlds most widely used sorting algorithm, and perhaps even the worlds most widely used algorithm of any kind... In computer science, Communicating Sequential Processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. ... CACM is an acronym that may stand for: California Association of Community Managers Inc. ... Robin Milner is a prominent British computer scientist. ... The Journal of the ACM (JACM) is the leading scientific journal of the Association for Computing Machinery (ACM) in the broad area of computer science. ... Sir Charles Antony Richard Hoare (Tony Hoare or C.A.R. Hoare, born January 11, 1934) is a British computer scientist, probably best known for the development of Quicksort, the worlds most widely used sorting algorithm, and perhaps even the worlds most widely used algorithm of any kind... The Springer-Verlag (pronounced SHPRING er FAIR lahk) was a worldwide publishing company base in Germany. ... ICALP, the International Colloquium on Automata, Languages and Programming is organized annually by the European Association for Theoretical Computer Science and held held in different locations around Europe. ...

External links

• Denotation Semantics by Lloyd Allison
• Structure of Programming Languages I: Denotational Semantics by Wolfgang Schreiner
• Denotational Semantics: A Methodology for Language Development by David Schmidt
• Presentation by Josh Cogliati
• HQL by H. Hernan Moraldo – complete denotational semantics of a small language