SCHEDULE OF TOPICS

This schedule should be regarded as a very rough plan that will almost certainly change, perhaps substantially, during the course of the semester. The readings listed may also change, if I find alternatives that I think better match my purposes.

• Administrative, Introduction (1 class, January 24)

• Specification of Programming Languages (1 class, Jan 26)
  • Introductory example: Language EXPRESSIONS
  • Concrete and abstract syntax
  • Specification of syntax
  • "Natural" and denotational semantics
  Reading:
  • C. Strachey, Fundamental Concepts in Programming Languages, Higher-Order and Symbolic Computation 13, 11-49, 2000
    (consists of previously unpublished, but highly influential material from a 1967 Summer School course given by Strachey).

• The Lambda Calculus (3 classes, Jan 31, Feb 2, 7)
  • Untyped lambda calculus, conversion and reduction
  • Recursion and fixed-point combinators
  • Evaluation strategies
  • Typed lambda calculus
  Reading:
  • Reade, Elements of Functional Programming, Chapter 12 (The Lambda Calculus and Combinators)
  • Barendregt and Barendsen, Introduction to Lambda Calculus, revised edition, March 2000 (Sections 1-6.)

• Functional programming I: Language LAMBDA (2 classes, Feb 9, 14)
  • The lambda calculus as a programming language
  • Patterns, clausal function definitions
  • Virtual machine implementation
  Reading:
  • The Mechanical Evaluation of Expressions, by P. Landin, The Computer Journal, 6:308-320, 1964.

• Functional programming II: Language FUNCTIONS (2 classes, Feb 16, 21)
  • Local declarations: let and local
  • Polymorphism
  • Algebraic datatypes

• Introduction to Standard ML (4 classes, Feb 23, 28, Mar 2, 7)
  Reading:
  • ML Primer, by Ryan Stansifer, Prentice Hall, 1992.
  • Introduction to Standard ML , by Robert Harper, Technical Report ECS-LFCS-86-14, Univ. of Edinburgh, Laboratory for Foundations of Computer Science, 1986.

• MIDTERM EXAM (1 class, Mar 23)

• SPRING BREAK (March 13-19)

• Using ML to Define Semantics (1 class, Mar 21)
  • Language EXPRESSIONS revisited
  • Algebraic semantics, compositionality
  • Errors and effects
  • Continuations
  Reading:
  • R. Tennent, The Denotational Semantics of Programming Languages, Communications of the ACM, 19(8), August, 1976.

• Imperative programming I: Language COMMANDS (2 classes, Mar 23, 28)
  • Variables, assignment, conditionals, and loops
  • Defining looping in terms of recursion
  Reading:
  • Revised report on the algorithmic language Algol 60, by P. Naur, et al, Communications of the ACM, 6:1-17, January 1963.

• Imperative programming II: Language BLOCKS, PROCS, and PARAMS (5 classes, March 30, Apr 4, 6, 11, 13)
  • Block structure
  • Environment and store
  • Procedures, recursion
  • Parameter passing

• Imperative programming III: Language EXCEPTIONS (2 classes, Apr 18, 20)
  • Static vs. dynamic scoping
  • Exception handling

• Types and type inference (4 classes, April 25, 27, May 2, 4)
  • Typing rules for language LAMBDA
  • Type inference for language LAMBDA
  Reading:
  • A Simple Algorithm and Proof for Type Inference, by Mitchell Wand, Fundamenta Informaticae 10(1987), pp. 115-122.
  • Principal type schemes for functional programs, by Luis Damas and Robin Milner, ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico, pages 207-212, 1982.