[Prev][Next][Index][Thread]
new course at Stanford
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.