new course at Stanford

To: types@theory.LCS.MIT.EDU
Subject: new course at Stanford
From: jcm@ra.stanford.edu (John Mitchell)
Date: Fri, 30 Sep 88 21:16:37 EDT
Sender: meyer@theory.LCS.MIT.EDU

Date: Thu, 29 Sep 88 17:23:37 PDT

Here is a tentative outline for a course I am teaching this
fall. I would be interested in comments, suggestions, and
outlines of similar courses taught elsewhere.

-------------


                       CS 258
         Introduction to Programming Language Theory
                     Fall 1988

                    
                  John Mitchell
               Stanford University


Course Outline

1. Introduction
	a. Overview of course
	b. The simple programming language PCF
	(typed lambda calculus with functions, pairs,
	integers, booleans and recursion)
	
2. Typed lambda calculus
	a. Context-sensitive syntax 
	b. Equations, proofs, and reduction rules
	c. Semantics, and soundness of the proof system
	d. Three examples of semantic models
	(set-theoretic, recursion-theoretic and 
	continuous hierarchies)

2. Algebraic data types
	a. Basic universal algebra
	b. Equations, soundness and completeness
	c. Rewrite rules, confluence and termination
	d. Initiality and induction

3. Fundamental theorems about typed lambda calculus
   over arbitrary algebraic data types
	a. Logical relations 
	b. Logical partial functions and equivalence
	   relations
	c. Completeness, confluence and normalization 
	d. Representation independence

4. PCF Revisited
	a. Reduction strategies and recursion
	b. Semantics, specification and recursion
	c. The full abstraction problem
	d. State and side-effects

5. Polymorphism and Data Abstraction
	a. Type inference and the programming 
		language ML
	b. Explicit polymorphism
	c. Abstract data types and existential types 

Time permitting, we will also discuss object-oriented
programming languages and inheritance.