BRICS · Contents · Programme

**A BRICS Mini-Course**

**October 14, 22 and 27, November 3, 1999**

**Lectures by
John C. Reynolds, John.Reynolds@cs.cmu.edu
**

**
**

This will be a survey of the denotational definitions of the meaning of type systems. Since the central problem with these definitions is that there are too many of them, we will look for connections and unifications among them. Ultimately, we want to know ``What do types (and domains) mean?''

The following is a tentative outline:

An Overview

- simply typed lambda calculus
- intrinsic and extrinsic semantics of types

A Review of Domain Theory

- complete partial orders and continuous functions
- continuous, algebraic, and consistent CPO's
- retractions, projections, and closures
- recursive domain isomorphisms

Logical Relations and Partial Equivalence Relations

- typed logical relations
- typeless logical relations
- PER's on natural numbers
- PER's on domains

Information Systems

- information systems as logics
- event systems
- qualitative domains and coherent spaces
- stable functions and the Berry ordering
- intersection types

Polymorphism and Parametricity

- retraction models
- PER models

### Thursday October 14, 1999, 15:00-17:00 in Auditorium D1

### Friday October 22, 1999, 14:00-16:00 in Auditorium D4

### Wednesday October 27, 1999, 15:00-17:00 in Auditorium D4

### Wednesday November 3, 1999, 15:00-17:00 in Auditorium D4