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)

Tentative outline:

Basic Domain Theory

The Simply Typed Lambda Calculus

The Untyped Lambda Calculus

Partial Equivalence Relations (PER's)

Retractions

Information Systems (IS's)

Intersection Types

Polymorphic Types

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