Instructor: Cormac Flanagan
Lectures: Tu/Th, 8:00am-9:45am,
Engineering 2 building, room 192
Office
Hours: After class, and Thursdays
11am-noon
Office: Engineering 2 building, room 367
Teaching Assistant: Jessica Gronski
(jgronski at cs.ucsc.edu)
TA Office Hours: Monday and Wednesday, 10-11am, Engineering 2
building, room 392
Newsgroup: ucsc.class.cmps203 on news server news.ucsc.edu
A sample induction proof by Faron Moller.
An example project report.
Lectures and
Notes
|
Day |
Date |
Lecture |
Topic |
Due |
|
Thurs |
9/22 |
1 |
Course Overview and
Motivation Operational Semantics of
ARITH (PDF) |
|
|
Tues |
9/27 |
2 |
Operational Semantics of
IMP (PDF) |
Hw 1 (from 9/22) Winskel Ch 1,2 |
|
Thurs |
9/29 |
3 |
Proof techniques (PDF) |
|
|
Tues |
10/4 |
4 |
More proof techniques (PDF) |
Hw 2 (from 9/27) Winskel Ch 3,4 |
|
Thurs |
10/6 |
5 |
Small-step semantics(PDF) |
|
|
Tues |
10/11 |
6 |
Small-step semantics for
IMP (PDF) |
Hw 3 (from 10/4) |
|
Thurs |
10/13 |
7 |
Axiomatic semantics (PDF) |
Winskel Ch 6 |
|
Tues |
10/18 |
8 |
Axiomatic semantics (same notes from last
class) |
Hw 4 (from 10/11) Dijkstra's Guarded Commands,
Nondeterminancy and Formal Derivation of Programs |
|
Thurs |
10/20 |
9 |
Extended Static Checking
(ppt) |
Project proposals due |
|
Tues |
10/25 |
10 |
Guest Lecture: Stephen Freund |
Winskel Ch 11 sections
1,2, 5,6,11 or Pierce Ch 5 |
|
Thurs |
10/27 |
11 |
Lambda calculus (pdf) |
Hw
5 (from 10/13) |
|
Tues |
11/1 |
12 |
Lambda calculus (same
notes from last class) |
|
|
Thurs |
11/3 |
13 |
Type systems |
Read Cardelli’s “Type
Systems” (sections 1,2, and 3) |
|
Tues |
11/8 |
14 |
Types systems (same
notes from last class) |
|
|
Thurs |
11/10 |
15 |
Advanced type systems (pdf) |
Read Cardelli’s “Type
Systems” (sections 4 and 5) or Pierce book, Chapters
8,9,11 |
|
Tues |
11/15 |
16 |
Hybrid type checking (paper) |
|
|
Thurs |
11/17 |
17 |
Student
presentations Casey Marshall * Survey of software
transactional memory Marinna Lee * Survey of language
design Suma Potluri * Survey of real time
garbage collection Eugene Mirkin * Survey of
parallelizing compilers Hsin-Chen Chiao * Survey of optimization
strategies Tim Kaldewey * Survey of real time
programming languages and extensions Jacob Telleen * Simply-typed lambda
calculus |
|
|
Tues |
11/22 |
18 |
Student
presentations Mark Deckert * Comparison of three
programming languages Nikhil Bobb * Implementation of
Obfuscator for IMP Kevin Greenan * Implementation of
multithreaded IMP Alex Yakushev * Implementation of IMP
with nondeterminism Jeff Hagen * Implementation of
string-based functional Ian Rickard * Implementation of
multithreaded IMP |
|
|
Thurs |
11/24 |
|
|
|
|
Tues |
11/29 |
19 |
Student
presentations John Wallerius * Implementation of
verifier for IMP Veronica Mayorga * Implementation of
multithreaded IMP Bogdan Alexe * Implementation of type
inference of the lambda-calculus Kevin Hullett * Implementation of the
Sluglog logic programming language language Anna Povzner * Implementation of CSP Anne Sullivan * Implementation of Lua |
|
|
Thurs |
12/1 |
20 |
Student
presentations Daniel Libicki * Definition of Glib Jennifer Flynn * Implementation of a
language with sets Damian Eads * Implementation of a
language with multiple dispatch Jordan Johnson * Implementation of a
language with multiple dispatch Colin Southwood * Implementation of a verifier
for IMP David Olsen * Implementation of
multithreaded IMP Jevgenia Smorgun * Survey of visual
programming languages Yuki Yamaguchi * Implementation of IMP
with CTL |
Project report |
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.
Required textbook:
·
Glynn Winskel,
"The Formal Semantics of Programming Languages: An Introduction",
MIT Press, 1993 ($43.45 from amazon.com)
Optional textbooks:
·
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 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.
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.
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.
The presentation should be
very short (10 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 3-4 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.
~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.
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.
Last updated: 22 September 2005