15-819A Denotational Semantics of Types - Spring 2000
Instructor: John Reynolds
TTh 10:30-11:50, WeH 4601
12 Units

DESCRIPTION: This will be a survey of the meanings given to type systems by denotational semantics using domains. Since the central problem is the perplexing variety of these meanings, we will look for connections and unifications among them. Ultimately, we want to know "What do types (and domains) really mean?"

CLASS NOTES (in postscript)

• Chapter 1 Categories and CPO's (February 15): A condensation of old notes from previous courses.
• Chapter 2 Some Varieties of Domains (February 16): The concept of "color" is used to unify the treatment of products, pullbacks, exponentiations, disjoint unions, lifting, and topping of various kinds of domain. This repeats some material of the previous chapter, but with greater unity and less category-theoretic formality.
• Chapter 3 Continuous and Algebraic Domains (April 17): The topology of domains, the way-below relation, continuous and algebraic domains, and their constructors.
• Chapter 4 Retractions, Projections, and Closures (April 17).
• Chapter 5 Intersection Types (preliminary version, April 25): Syntax and intrinsic semantics.

Tentative outline:

Basic Domain Theory

• complete partial orders (CPO's) and continuous functions
• continuous, algebraic, and consistent CPO's
• products, coproducts, and exponentiation
• recursion and the least fixed-point theorem
• recursive types and the inverse limit construction

The Simply Typed Lambda Calculus

• syntax and reduction rules
• reduction rules
• an intrinsic set-theoretic semantics
• an intrinsic domain-theoretic semantics
• the logical relations theorem

The Untyped Lambda Calculus

• syntax and reduction rules
• domain-theoretic semantics

Partial Equivalence Relations (PER's)

• PER's on the natural numbers
• PER's on domains
• an extrinsic semantics of typed lambda calculus using PER's
• directed complete relations and recursion
• relating intrinsic and extrinsic semantics
• problems with recursive types

Retractions

• retractions, projections, and closures
• retraction semantics of types
• recursive types via retractions
• relating retractions and PER's: bracketing

Information Systems (IS's)

• IS's as logics
• the connection with domains
• models of IS's
• recursively defined IS's
• qualitative domains and coherent spaces
• stable functions and the Berry ordering

Intersection Types

• an intrinsic semantics using pullbacks
• an extrinsic semantics using IS's

Polymorphic Types

• retraction models
• PER models
• parametricity

TEXT: Class notes and papers to be supplied by the instructor. There is also an optional textbook: Domains and Lambda-Calculi, by R. M. Amadio and P.-L. Curien, Cambridge University Press, 1999.

PREREQUISITES: CS 711 or permission of the instructor. Both creditors and auditors must register. John.Reynolds@cs.cmu.edu (home page)
last updated April 25, 2000