Instructor: Cormac Flanagan

Lectures: Tu/Th, 10:00am-11:45am, Engineering 2 building, room 194

Office Hours: After class, and Tuesdays 1:30-2:30pm, in Engineering 2 building, room 367

If you have trouble installing Ocaml on your own computer, you can use sundance.cse.ucsc.edu, where it is pre-installed.

NEW: homeworkcode

NEW: Project and Presentation Schedule

Newsgroup: Please subscribe to the class email list: http://groups.google.com/group/ucsc-cmps203-fall07

Helpful links: Some code snippets and the Ocaml release

A sample induction proof by Faron Moller.

CS203 is designed to acquaint graduate students with basic ideas behind modern programming language design.

The first part of this graduate-level course focuses on the study of the semantics of a variety of programming language constructs. We will study operational semantics, which are a way to formalize the intended execution and implementation of languages, and axiomatic semantics, which is useful in developing as well as verifying programs. We will apply these techniques to imperative, functional and object-oriented languages. For this part of the course we will follow the presentation of these topics from Glynn Winskel's “The Formal Semantics of Programming Languages”.

The second part of this course covers the basic techniques used in the study of type systems for programming languages. We will start our study with the simply typed lambda calculus and continue with more advanced features such as types for imperative features and exceptions, parametric polymorphism, existential types for use in abstraction and module systems, and dependent types. A good reference for this part of the course is John Mitchell's “Foundations for Programming Languages”.

The last part of the course covers special topics, occasionally presented by expert invited speakers, drawn from recent research in the semantics of object-oriented languages, abstract interpretation and applications of program semantics in program analysis and verification. This part of the course will also cover several novel applications of ideas from language semantics to system security in the presence of untrusted code, such as perhaps type systems for securing the flow of information.

In addition to the topics studies in class, students will have the opportunity to consider other related topics of interest in the form of a course project.

The prerequisites for this course are programming and mathematical experience. The ideal programming experience is practical exposure to several different programming languages, such as C, ML, Prolog and Java. The ideal mathematical experience is knowledge of mathematical logic and ability to construct rigorous proofs (in particular by structural induction). None of these prerequisites are strict. However, your desire to be exposed to this material is very important. In the past a small number of undergraduates have been able to complete the course.

As mentioned in the course description above a number of textbooks will be used in this course. All of these textbooks will be placed on reserve at the library. Copies of the lecture notes will also be made available on the course home page.

1. Glynn Winskel, “The Formal Semantics of Programming Languages: An Introduction”, MIT Press, 1993 ($43.45 from amazon.com)

1. John C. Mitchell, “Foundations for Programming Languages”, MIT Press, 1996.
2. Benjamin Pierce. “Types and Programming Languages”, MIT Press, 2002.

There will be some homework assignments, often mathematical in nature. Collaboration in pairs on the homework is ok, as long as you clearly identify on your submitted homework whom you worked with.

The final project is intended to give you hands on experience with the material taught in the course and also to allow you to explore in more depth a topic of your own interest. Acceptable projects can be a programming project, a survey of recent research on some relevant topic, or a small research paper. Everybody must select a project and write a very short (one to two pages) proposal arguing what is expected to be learned from the project (why is it interesting to you) and giving a work schedule. Make sure to budget time for writing a short paper describing the project and for preparing a short (10-15 minute) presentation during the last week or two of classes. Projects can be individual or in small groups.

NEW: Project Proposals

The main goal of the project is to allow you to customize the content of the course to your own interests. The goal is not to force you all to produce novel results in one semester.

1. The project proposal is due on October 18th. This should be a 1 to 2 pages paper describing what you plan to do. Please hand it in on paper at the start of class. The main purpose of this is to allow me to give you feedback on the feasibility of the project (in case you propose to solve the halting problem by the end of the semester )
2. During the month of November I will announce a schedule of 10 minute presentations during the last four class periods. Please let me know if you have a preference.
3. The final report for your project is due on paper at the start of the last class.

More details about the expected scale of the project and the various kinds of projects (survey, implementation, research) will be discussed in class.

The project report should have an Introduction describing the tackled problem, its motivation and a very brief summary of the accomplishment. Then you should write a description of your notations if they are different from what we used in class. Then you continue with the body of the material. The paper should end with a Conclusion putting the perspective the accomplishment of the project and mentioning the open problems and with a Bibliography of cited papers. Research papers should also have a Related Work section in which they compare the work with previous research results. The paper should be typeset and made available in electronic form.

An example project report.

The presentation should be short (10-15 minutes) and should describe in few details what the problem was, what the difficulties were and what was accomplished or learned. You will find it much easier to prepare the talk using slides (perhaps 4-6 slides excluding the title, depending on your speed). While preparing the talk keep in mind who your audience is: your colleagues who are eager to find out (1) about new exciting facets of programming languages and (2) how much fun you had. Plan to motivate the project (why is it important) and to describe what you learned from it. Keep in mind that your colleagues have not read all the papers that you have read to do the project.

You will need to have a “buddy” for your presentation, who listens to a full-length dry run of your presentation before your class presentation, and gives you detailed, constructive feedback on how to improve your presentation. Please remember to thank your buddy by name as part of your presentation.

1. small-step operational semantics and implementation for a more interesting language than IMP, perhaps
   1. a small, multithreaded language,
   2. a logic programming language similar to Prolog (somewhat harder),
   3. a language with non-determinism of some sort.
   • Your implementation could test a single random path, many random paths, or all possible paths (ie a model checker). You could add a graphical output (perhaps with the “dot” graph drawing tool) of the state space.
2. An implementation of a checker based on axiomatic semantics. This involves two stages:
   1. translating a program to a logical formula, and
   2. checking validity of that formula.
   • The second stage could be done by an off-the-shelf theorem prover such as Simplify. Read the “Extended Static Checking” paper from PLDI'00 for more ideas.
3. An implementation of a type checker for some small but interesting language.
4. An implementation of a type inference algorithm, perhaps for simply-typed lambda-calculus with polymorphism.
5. Perhaps something related to AJAX and Web 2.0. Some good ideas and pointers are here. JavaScript is a functional/object-oriented language, a little bit like Ocaml without types.
6. There are lots of interesting issues related to concurrency. A reading list of important papers is in the CMPS253 web page, which might be a starting point for a survey, research, or implementation project.