Re: domains for typed lambda calculi

Jose Juan Mendoza Rodriguez <me@xxxxxxxxxxx> wrote:
Chapters 2 and 8 of Andrea Asperti, Giuseppe Longo.
Categories, Types and Structures. M.I.T. Press, 1991 available at
http://www.di.ens.fr/users/longo/download.html
http://www.cs.unibo.it/~asperti/PAPERS/book.pdf
discuss the (categorical) semantics of typed-lambda calculus
based on Scott domains (domains = types, continuous functions = terms).
Chapter 8 can be read just after section 2.4, or even 2.3 (no need to
learn complex categorical notions). This semantics is based on the
work of Plotkin,

Gordon D. Plotkin. Pisa Notes (On Domain Theory). Department of
Computer Science, University of Edinburgh, 1983 available at
http://homepages.inf.ed.ac.uk/gdp/publications/Domains.ps

Chapters 7 and 8 of Jaap Van Oosten. Basic Category Theory.
http://www.math.uu.nl/people/jvoosten/syllabi/catsmoeder.ps.gz
http://www.math.uu.nl/people/jvoosten/syllabi/catsmoeder.pdf
also contain similar material, but Van Oosten is definitely more
mathematical and much less "computer-oriented".

There are many more texts available on the web on this topic,
but these are my preferred ones (PS. Be aware that the Asperti/Longo
text contains some errata in the exercises).

Thank you very much, Jose.
That's exactly what I was looking for.
--
John Forkosh ( mailto: j@xxxxx where j=john and f=forkosh )
.

Relevant Pages

  • Re: Topology of proof
    ... please excuse ... is often called domain theory ... (or alternatively fixed-point semantics ... by amadio and curien ...
    (sci.logic)
  • Re: domains for typed lambda calculi
    ... Andrea Asperti, Giuseppe Longo. ... discuss the semantics of typed-lambda calculus ... This semantics is based on the ... Gordon D. Plotkin. ...
    (comp.theory)