Resources for learning domain theory?

Question

I'm a computer programmer who's caught on to denotational semantics. I mostly work with Ruby, JavaScript and C, but I know a little Haskell and ML. I've taken my first steps towards reasoning about what my software means, but my knowledge of domain theory is weak. DCPOs, chains, new notation – can you recommend a coherent introduction to this stuff?

Answer 1

The book recommended by jef is the domain-theory bible. It may be a bit overwhelming for a beginner. For an easier and more compressed introduction I recommend that you have a look at Abramsky and Jung's chapter on domain theory from the Handbook of Logic in Computer Science. It is available in gzipped Postscript from Achim's home page, and CiteSeerX has it in PDF here.

Answer 2

Semantics with Applications: An Appetizer by Hanne Riis Nielson and Flemming Nielson provides a rudimentary introduction, also linking denotational semantics to program analysis via abstract interpretation. Plotkin's notes are excellent, more comprehensive, and more theoretically bent.

Answer 3

http://www.amazon.com/exec/obidos/ASIN/0521803381/

I read this book for a course when I was an undergraduate and it is a very good introduction for all the things you mentioned.

Answer 4

I used the book The Formal Semantics of Programming Languages by G. Winskel for an undergraduate course, and I found it a reasonably good introduction to the topic; it also covers operational semantics and its relationship with denotational semantics, which I found quite enlightening since the former one is probably easier to grasp initially.

Answer 5

Another good book that teaches the ropes of domain theory for a beginner is Thomas Streicher's "Domain-Theoretic Foundations of Functional Programming", World Scientific. I highly recommend this book because of its clarity and rigour. Please look up the link at http://www.worldscientific.com/worldscibooks/10.1142/6284 for information on this book. The functional language it works with is a prototypical simply-typed lambda calculus, called PCF (Programming language for Computable Functionals). The domain theory developed in it and the denotational semantics defined is systematic in its organization.