Types and Type-free λ-Calculus

Denotational semantics started in Oxford in late 1969.  It was hoped that domain theory would provide a basis both for recursive definitions in programs and recursive definitions of semantical structures.  Early troubles were encountered in using tops and bottoms, and soon researchers turned to operational semantics. Others wanted to expand work to communicating and parallel processes. Axiomatic and synthetic theories did not solve the problems, and as a result much research effort in domain theory faded.  Late work by Reynolds and collaborators, however, has opened up new and promising approaches for programming-language semantics. Perhaps the much simplified modeling using enumeration operators can spark some new investigations, especially since it is so easy to add a rich type structure to the calculus.  A later talk will show how to add random elements to this model using a Boolean-valued interpretation.