CS258: Introduction to Programming Language Theory

Winter 2006-07

Class Location: Bldg. 260, Room 113 [map link]

Class Timings: Tuesdays and Thursdays, 3:15-4:30PM

Office Hours: Tuesdays and Fridays, 1-2PM, Gates 468

Course Assistant: Arnab Roy

Office Hours: Wednesdays and Thursdays, 2-3PM, Gates 490

Student Mailing list:               cs258-win0607-students@lists.stanford.edu
Staff Mailing list:                 cs258-win0607-staff@lists.stanford.edu
Common Mailing list:           cs258-win0607-all@lists.stanford.edu

Course Newsgroup: su.class.cs258

Summary:

This course introduces the basic concepts and methods of the theory of programming languages. This year's offering will focus on type systems and operational semantics. Commonly used language features including simple and recursive functions, products and records, recursive structures (lists, trees), polymorphism, data abstraction, subtyping and object systems will be studied from a type-theoretic standpoint. An application of these methods towards establishing the type safety of Java will be presented. A discussion of axiomatic and denotational semantics will also be included to provide a holistic picture of the field. These approaches will be illustrated using an imperative language of while programs. The relations between the three forms of semantics will be touched upon.

Prerequisites:

The prerequisites are familiarity with programming concepts and basic notions of mathematical logic (formulas, proof systems and semantics). In addition, the course requires the proverbial "appropriate level of mathematical sophistication" associated with rigorous proof. Translated into course numbers, the requirements are approximately (i) CS 157 or Phil 151/251 for mathematical logic, (ii) some course in programming, such as CS 106, and (iii) familiarity with computability theory, at approximately the level of CS 154.

Course Syllabus, Schedule and Notes

Announcements:

· Use this template for scribing notes.

· Tutorial session on Tuesday, Jan. 30, 4:45-6PM. Location: Gates 498

· Homework 1 is out; due on Monday, Feb 12, 5PM in Gates 490.

· Homework 1 tex sources: hw01.tex, proof.sty

· On Recursion

· Homework 2 is out; due on Monday, Feb 26, 5PM in Gates 490.

· Homework 2 tex sources: hw02.tex, proof.sty

· Homework 3 is out; due on Monday, Mar 12, 5PM in Gates 490.

· Homework 3 tex sources: hw03.tex, proof.sty

· Equational Reasoning