Programming Languages

Instructor: Cormac Flanagan
Lectures: Tu/Th, 12:00pm-1:45pm, Social Sciences 2 167

Office Hours: Tuesday 4:30-5:30pm, Thursdays 8:30-9:30am, or by appointment
Office: Baskin Engineering 353A

Teaching Assistant: Aaron Tomb
TA Office Hours: Wednesday, 12:00-1:30pm, Engineering 2 Building, room 392

Newsgroup: ucsc.class.cmps203 on news server news.ucsc.edu

Some sample Objective Caml code for big step operational semantics of ARITH. Also, some code for dealing with overflow, and a small step semantics.

Day	Date	Lecture	Topic	Due
Thurs	9/23	1	Course Overview and Motivation (pdf)
Tues	9/28	2	Operational Semantics of ARITH (pdf)
Thurs	9/30	3	Operational Semantics of IMP (pdf)	Hw 1
Tues	10/5	4	IMP (continued) and proof techniques (pdf)	Winskel Ch 3+4 Faron Moller's sample proof by induction
Thurs	10/7	5	- proof techniques continued, same lecture notes	Hw 2
Tues	10/12	6	- proof techniques continued
Thurs	10/14	7	Axiomatic semantics (pdf)
Tues	10/19	8	- axiomatic semantics continued	Hw 3 Winskel, Ch. 6.1-6.4 Hoare's "An axiomatic basis for computer programming" Floyd's "Assigning meaning to programs"
Thurs	10/21	9	Extended Static Checking (ppt)	Project proposals due Dijkstra's Guarded Commands, Nondeterminancy and Formal Derivation of Programs Extended Static Checking for Java
Tues	10/26	10	Lambda calculus (pdf)	Hw 4 Pierce's "Foundational calculi for programming languages" (pages 1-10) Hudak's "Conception, evolution, and application of functional programming languages" (to end section 1.5)
Thurs	10/28	11	- lambda calculus continued
Tues	11/2	12	Type systems (pdf)	Hw 5 Cardelli's "Type systems" (sections 1, 2, and 3)
Thurs	11/4	13	- type systems continued (pdf)	Cardelli's "Type systems" (section 4)
Tues	11/9	14	- type systems continued (pdf)	Rest of Cardelli's "Type systems"
Thurs	11/11		Holiday
Tues	11/16	15	- type systems continued, polymorphism (pdf)	Hw 6
Thurs	11/18	16	Concurrency and applications (pdf)
Tues	11/23	17	Model Checking and Program Analysis	Richard Hamming: You and Your Research Andrew Birrell: An Introduction to Programming with Threads
Thurs	11/25		Holiday - thanksgiving
Tues	11/30	18	Student presentations Simon Goldrei: The Design, Implementation and Use of DSLs: A survey slides report Xing Ji: Survey of typed assembly languages slides report Josh Spiegel: Survey of XML query languages slides Vesselin Diev: Survey of static validation of dynamic XML slides report Emmanuel Pontikakis: XML XPATH semantics slides report Vadim Von Brzeski: Survey of languages for quantum computing slides report Prachi Tiwari: Survey of atomicity in concurrent programming languages slides report Jerry Yee: Survey of computer graphics programming languages slides report Oliver Wang: Graphics hardware programming languages slides report Karl Schnaitter: Extending primitive types slides report Avik Chaudhuri: Mechanics of the pi-calculus and variants slides report Sean Halle: Code time parallel programming platform report
Thurs	12/2	19	Student presentations Mark Storer: Security in IMP through abstract semantics and static evaluation slides report Kristal Pollack: Extending IMP to support threads with race detection report Philip Zigoris: Validating programs with examples: theoretical exploration slides report Jessica Gronski: Hoare logic for reasoning about multithreaded programs slides report Haward Jie and Shivkumar Shivaji: Temporal-safety proofs in file system development slides report John Wallerius: CVC-lite validity checking of Hoare triples slides Vishwanath Raman: Pointer Analysis - A Survey slides report Kenn Knowles: Limited but tractable type inference against races slides report Eric Poblenz: Analysis of a type system for computational biology simulations report Suratna Budalakoti: A small programming language for handling graphs slides Robert Hero: Automatic Parallelization of OpenGL code slides report Alessandro Temil: Automated WCET estimation for a simple imperative programming language slides Fima Leshinsky: Survey of code validation and security in Java Also: Ranjit Jhala from UC Berkeley on BLAST Software Engineering Lab, Engineering 2 Building, room 392, at 2pm.	Project report

Course description:

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 structural operational semantics as a way to formalize the intended execution and implementation of languages, axiomatic semantics, useful in developing as well as verifying programs, and denotational semantics, whose deep mathematical underpinnings make it the most versatile of all. 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, most often in the form of a survey of recent research on a topic of interest.

Course prerequisites:

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.

Textbooks:

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.

Recommended	Glynn Winskel, "The Formal Semantics of Programming Languages: An Introduction", MIT Pres, 1993
	John C. Mitchell, "Foundations for Programming Languages", MIT Press, 1996.
	Benjamin Pierce. “Types and Programming Languages”, MIT Press, 2002.

Homework Assignments:

There will be some homework assignments, often mathematical in nature.

The Project

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 minute) presentation during the last week of classes. Projects can be individual or in small groups.

Goal

Dates

• The project proposal is due on October 21th. 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 :-))
• During the month of November I will announce a schedule of 10 minute presentations during the class times on November 30 and December 2. Please let me know if you have a preference.
• You can continue to work on the paper and the implementation until December 2 when the final versions of your papers are due on paper at the start of class.

Project paper

The presentation

Project suggestions

• small-step operational semantics and implementation for a more interesting language than IMP, perhaps
  • a small, multithreaded language,
  • a logic programming language similar to Prolog,
  • 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.
• An implementation of a checker based on axiomatic semantics. This involves two stages:
  • translating a program to a logical formula, and
  • 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.
• An implementation of a type checker for some small but interesting language.
• An implementation of a type inference algorithm, perhaps for simply-typed lambda-calculus with polymorphism.

Last updated: 2004-10-12