Related Research Articles
Sir Charles Antony Richard Hoare is a British computer scientist who has made foundational contributions to programming languages, algorithms, operating systems, formal verification, and concurrent computing. His work earned him the Turing Award, usually regarded as the highest distinction in computer science, in 1980.
In computer science, denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects that describe the meanings of expressions from the languages. Other approaches providing formal semantics of programming languages include axiomatic semantics and operational semantics.
In computer science, a compiler-compiler or compiler generator is a programming tool that creates a parser, interpreter, or compiler from some form of formal description of a programming language and machine.
Dana Stewart Scott is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, California. His work on automata theory earned him the Turing Award in 1976, while his collaborative work with Christopher Strachey in the 1970s laid the foundations of modern approaches to the semantics of programming languages. He has worked also on modal logic, topology, and category theory.
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. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.
In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages. It does so by evaluating the meaning of syntactically valid strings defined by a specific programming language, showing the computation involved. In such a case that the evaluation would be of syntactically invalid strings, the result would be non-computation. Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will be executed on a certain platform, hence creating a model of computation.
In computer science, a continuation is an abstract representation of the control state of a computer program. A continuation implements (reifies) the program control state, i.e. the continuation is a data structure that represents the computational process at a given point in the process's execution; the created data structure can be accessed by the programming language, instead of being hidden in the runtime environment. Continuations are useful for encoding other control mechanisms in programming languages such as exceptions, generators, coroutines, and so on.
Peter John Landin was a British computer scientist. He was one of the first to realise that the lambda calculus could be used to model a programming language, an insight that is essential to development of both functional programming and denotational semantics.
CPL is a multi-paradigm programming language, that was developed in the early 1960s. It is an early ancestor of the C language via the BCPL and B languages.
Samson Abramsky is a computer scientist who holds the Christopher Strachey Professorship at the Department of Computer Science, University of Oxford. He has made contributions to the areas of domain theory, the lazy lambda calculus, strictness analysis, concurrency theory, interaction categories, geometry of interaction, game semantics and quantum computing.
Christopher S. Strachey was a British computer scientist. He was one of the founders of denotational semantics, and a pioneer in programming language design and computer time-sharing. He has also been credited as possibly being the first developer – with recorded evidence – of a video game. He was a member of the Strachey family, prominent in government, arts, administration, and academia.
Joseph E. Stoy is a British computer scientist. He originally studied physics at Oxford University. Early in his career, in the 1970s, he worked on denotational semantics with Christopher Strachey in the Programming Research Group at the Oxford University Computing Laboratory. He was a Fellow of Balliol College, Oxford. He has also spent time at MIT in the United States. In 2003, he co-founded Bluespec, Inc.
In computer science, unbounded nondeterminism or 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. 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.
Gordon David Plotkin, is a theoretical computer scientist in the School of Informatics at the University of Edinburgh. Plotkin is probably best known for his introduction of structural operational semantics (SOS) and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics were very influential. He has contributed to many other areas of computer science.
In denotational semantics and domain theory, power domains are domains of nondeterministic and concurrent computations.
The denotational semantics of the Actor model is the subject of denotational domain theory for Actors. The historical development of this subject is recounted in [Hewitt 2008b].
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages and of their individual features. It falls within the discipline of computer science, both depending on and affecting mathematics, software engineering, linguistics and even cognitive science. It has become a well-recognized branch of computer science, and an active research area, with results published in numerous journals dedicated to PLT, as well as in general computer science and engineering publications.
David Anthony Watt is a British computer scientist.
William D. Clinger is an associate professor in the Khoury College of Computer Sciences at Northeastern University. He is known for his work on higher-order and functional programming languages, and for extensive contributions in helping create and implement international technical standards for the programming language Scheme via the Institute of Electrical and Electronics Engineers (IEEE) and American National Standards Institute (ANSI). Clinger was an editor of the second through fifth Revised Reports on Scheme (R2RS – R5RS), and an invited speaker on Scheme at the Lisp50 conference celebrating the 50th birthday of the language Lisp. He has been on the faculty at Northeastern University since 1994.
References
- ↑ Peter Mosses, "SIS: A Compiler-Generator System Using Denotational Semantics," Report 78-4-3, Dept. of Computer Science, University of Aarhus, Denmark, June 1978
