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. |
Contents
Interpretation of Acalculi in CCCs | 71 |
The Language PCF | 124 |
Domain equations | 144 |
Values and computations | 168 |
XV | 185 |
Powerdomains | 200 |
Stone duality | 215 |
Dependent and second order types | 240 |
Sequentiality | 341 |
43 | 360 |
48 | 373 |
Domains and realizability | 388 |
Functions and processes | 421 |
Summary of recursion theory | 449 |
469 | |
473 | |
Other editions - View all
Common terms and phrases
A-calculus abstract adjoint algebraic bifinite domains bisimulation bistructures call-by-value called cartesian closed cartesian closed category cds's Chu space closed terms closure coherence spaces compact coprime compact elements complete computation consider construction context continuous functions coprime dcpo dcpo's defined as follows definition denote e₁ equations equivalence evaluation Exercise exists extensional figure finite fixpoint following properties full subcategory function f functor given glb's Hence hypercoherences implies induction interpretation isomorphic L-domains lemma linear linear logic logic lub's meet cpo's monad monotonic morphism notion observe open sets operator output partial order per's pointwise pointwise ordering poset preorder PROOF HINT proposition prove recursive redex reduction relation retraction rules Scott domains Scott topology semantics semi-lattice sequential algorithms sequential functions simply typed stable functions structure subset Suppose T-algebra terminal object theorem topology upper bound valof variables X-terms
Popular passages
Page 470 - Blass. A game semantics for linear logic. Annals of Pure and Applied Logic, 56:183-220, 1992.