Domains and Lambda-CalculiThis book describes the mathematical aspects of the semantics of programming languages. The main goals are to provide formal tools to assess the meaning of programming constructs in both a language-independent and a machine-independent way and to prove properties about programs, such as whether they terminate, or whether their result is a solution of the problem they are supposed to solve. In order to achieve this the authors first present, in an elementary and unified way, the theory of certain topological spaces that have proved of use in the modeling of various families of typed lambda calculi considered as core programming languages and as meta-languages for denotational semantics. This theory is now known as Domain Theory, and was founded as a subject by Scott and Plotkin. One of the main concerns is to establish links between mathematical structures and more syntactic approaches to semantics, often referred to as operational semantics, which is also described. This dual approach has the double advantage of motivating computer scientists to do some mathematics and of interesting mathematicians in unfamiliar application areas from computer science. |
What people are saying - Write a review
We haven't found any reviews in the usual places.
Contents
| 22 | |
| 43 | |
| 71 | |
The Language PCF | 124 |
Domain equations | 144 |
Values and computations | 168 |
Powerdomains | 200 |
Stone duality | 215 |
Stability | 270 |
Towards linear logic | 301 |
Sequentiality | 341 |
Domains and realizability | 388 |
Functions and processes | 421 |
Summary of recursion theory | 449 |
References and bibliography | 469 |
Index | 480 |
Other editions - View all
Common terms and phrases
7r-calculus abstract adjoint algebraic basic bifinite domains bisimulation bistructures calculus call-by-value called cartesian closed cartesian closed category chapter Chu space closed term coherence spaces compact coprime compact elements computation consider construction context continuous functions coprime dcpo dcpo's defined as follows definition denote equations equivalence evaluation Exercise exists extensional figure finite fixpoint following properties full subcategory function f functor gib's given Hence hypercoherence implies induction injection-projection pairs interpretation isomorphic L-domains lemma linear linear logic logic lub's meet cpo's monad monotonic morphism notion observe open sets operational semantics operator output partial order per's pointwise pointwise ordering poset preorder Proof hint proposition prove recursive redex reduction relation retraction rules satisfies Scott domains Scott topology semantics semi-lattice sequential algorithms stable functions structure subset Suppose terminal object theorem theory topology trace(f untyped upper bound valof variables
Popular passages
Page 471 - Blass. A game semantics for linear logic. Annals of Pure and Applied Logic, 56:183-220, 1992.
Page ii - J.-J. Ch. Meyer &; W. van der Hoek Epistemic Logic for AI and Computer Science 42.
Page 8 - Hausdorff: if x ^ y, then there exist disjoint open sets U and V such that x £ U and y € V.
Page 161 - The proof of this theorem is an immediate consequence of the following lemmas.
Page 43 - — »" is contravariant in its first argument and covariant in its second argument.
Page 417 - ... restructured and new functionalities are added. Such theories support an incremental design of software systems and establish under which conditions the programmer is allowed to reuse previously created modules. Such reuse may require the introduction of explicit or implicit coercions whose effect on the semantics of the program has to be clearly understood by the programmer. A formalization of this concept in the context of typed languages can be given in two steps...
Page 348 - The following example shows that this is not true in general. Let X...
Page 376 - natural' algorithm that computes the semantic function IJ (cf. exercise 14.3.53) and denoting likewise by BT the minimum algorithm computing BT, does the equality (of algorithms) [_] = [_J o BT hold? In other words, does the semantic evaluation respect the indications of sequentiality provided by the syntax itself? (2) If a and a' are two definable algorithms such that a < a', can we find N and N' such that N < N' (in the sense of definition 2.3.1), a = [JV], and a
Page 350 - We first remark that the last assertion of (1) follows from the others, since if x ^ z, then the existence of a chain between x and y as described in the statement entails that u or w is of type 'valof '. Let s and t be two proofs of xc1 and zc1 in a, respectively; here is the detail of s until the first enabling of type 'output...
Bibliographic information
| Title | Domains and Lambda-Calculi Issue 46 of Cambridge Tracts in Theoretical Computer Science, ISSN 0956-9103 |
| Authors | Roberto M. Amadio, Pierre-Louis Curien, Amadio Roberto M. |
| Edition | illustrated, reprint |
| Publisher | Cambridge University Press, 1998 |
| ISBN | 0521622778, 9780521622776 |
| Length | 484 pages |
| Subjects | › › Computers / Programming Languages / General Mathematics / Discrete Mathematics Mathematics / History & Philosophy Mathematics / Logic |
| Export Citation | BiBTeX EndNote RefMan |