Introduction: This course has three main themes:

• the design and implementation of programming languages,
• the use of formalism within the context of programming and programming languages, and
• the relationship between problem solving and program-language design.

Formalism provides clarity for programming in two ways.

• Formal language specification clarifies both the syntax of a language and its semantics -- the correct format of programs and what those programs mean. In working with a language, programmers should not have to conduct experiments to determine what constructs are legal or how the language will behave on a specific machine in a particular environment. Rather, a formal specification of both syntax and semantics can clarify alternatives, avoid ambiguities, and establish standards. Several approaches have been developed for formal specification, and each has its proponents. About one-third of the way through this course, we will examine important elements of denotational semantics as one popular approach to this formal specification.

• To utilize programming languages effectively, programmers must be able to write clean, clear, and correct code. Formal reasoning about programs can be very helpful in this process. Specifically, program verification involves two basic goals. First, techniques are developed in order to prove programs are correct, using formal mathematical methods. Second, the process of writing proofs is combined with the developing programs, so that software development involves the simultaneous production of computer programs and the proofs that they are correct. The course generally will explore program verification on Monday each week.

Henry M. Walker

Office: Science 2420
Telephone: extension 4208
E-mail: walker@cs.grinnell.edu

Office hours are posted weekly on the bulletin board outside Science 2420, with additional hours possible by appointment. You may reserve a half hour meeting by signing up on the weekly schedule, but please sign up at least a day in advance.

John Mitchell, Concepts in Programming Languages, Cambridge University Press, 2003.
The author is maintaining a supporting web site at http://theory.stanford.edu/people/jcm/books.html

David Gries, The Science of Programming, Springer-Verlag, New York, 1981.
This is the classical text on the subject of program verification.

Students may find the following references useful:

• Andrew Cumming, A Gentle Introduction to ML, Napier University, Edinburgh, 1998.

• Robert Harper, Programming in Standard ML, School of Computer Science, Carnegie Mellon University, 2000.

  Older, 1993 version in postscript format

• Chris Stone Information about Standard ML, School of Computer Science, Carnegie Mellon University, 1998.

• Daniel Diaz, GNU Prolog: A Native Prolog Compiler with Constraint Solving over Finite Domains, September 25, 2002.

• Patrick Blackburn, Johan Bos and Kristina Striegnitz, Learn Prolog Now!, tutorial, July 18, 2001.

While the schedule for this course is expected to evolve, a Tentative Class Schedule is available in .dvi , postscript , and pdf formats.

As this schedule suggests, each day in a typical week for this course has a different theme:

• Monday: Program verification
• Wednesday: Programming language issues
• Friday: Questions and group work, based on the week's material

Note: If you are logged into the departmental network and want a copy printed, click duerer to have a copy printed on the printer duerer, and click pacioli to have a copy printed on the printer pacioli .

Course Work will involve a combination of the following activities.

• Written Assignments Since the learning of concepts and technical details requires hands-on experience, homework will be assigned regularly.

• Group Work: Friday activities often will involve work in groups, and those groups will prepare materials or make oral presentations.

• Programs: Several programming assignments will be due throughout the semester.

• Tests: Take-home tests may be scheduled during the semester.

• Exam: The final examination will follow an oral format and will be scheduled with individual students during exam week.

Late Penalty: Work is due at the start of class on the date specified in the assignment. A penalty of 33 1/3 % per class meeting will be assessed on any work turned in late, even work submitted at the end of a class. Thus, work turned in 4 days late will be weighted -33 1/3 %; since a negative score reduces a semester total, it is better not to turn the work in at all.
Exception: Deadlines for programming problems and laboratory exercises are automatically extended at least one class day if MathLAN is down for an unscheduled period of 3 or more hours during the week preceding the assignment due date. (In such cases, however, deadlines for written assignments are not extended.)

Absolute Deadline: All homework must be turned in by Friday, May 7 at 5:00 pm.
Don't even think about asking for an extension!

The work in this course is split between individual and group work. The rules for collaboration on written assignments will be given for each assignment.

The final grade will be based upon each student's demonstration of his or her understanding of and facility in programming, not on the performance of the class as a whole nor on a strict percentile basis. While some flexibility may be possible in determining a final semester grade, the following percentages provide a first approximation for the relative weights attached to various activities in this course.

Assignments from Mitchell's Text:

20%

Assignments from Gries' Text:

40%

Group Work:

20%

Exam:

20%

This document is available on the World Wide Web as

     http://www.walker.cs.grinnell.edu/courses/302.sp04/index.html

created December 2, 2003 last revised May 3, 2004
For more information, please contact Henry M. Walker at walker@cs.grinnell.edu.