CS-430: Formal Semantics

 

Syllabus
Lecture Slides
Learning Haskell
Problem Set 1
Problem Set 2
Problem Set 3
Problem Set 4
Problem Set 5
Problem Set 6
Problem Set 7
Problem Set 8
Problem Set 9

Fall 2007 Course Overview:

CS-430 / CS-530 teaches the formal semantics of programming languages.  That is, a mathematically rigorous description of what a computer program means.  The course should be useful to anyone who is serious about programming, and is essential for anyone planning either to do research in programming languages or to design a programming language.  The course is intended to accomplish two things:

  1. Familiarize the student with the most common methods for specifying formal semantics.  In particular, the denotational, operational, and axiomatic approaches.  This will give the student the necessary tools and experience to understand semantics specifications and to develop new ones for new languages.
     
  2. Survey existing language features to provide the student with a deep understanding of what these language features really mean, what they do, and how they compare to one another.  This will enable the student to better evaluate existing programming languages and new ones as they are developed.

The course will be mostly mathematical in nature, but from time to time we will also use a functional language (Haskell) to prototype semantics specifications (in effect writing interpreters for several different languages).  This is a useful exercise that helps make the ideas more concrete.

Prerequisites:

You should have taken CS-201 and CS-202 (or equivalents), and have a couple of years of programming experience.  CS-223 and CS-323 (or equivalents) are also recommended, but not required.

Meeting time and place:

Tuesday/Thursday, 1:00-2:15 PM,  in  Room 500 AKW.
 

Instructor: Teaching Fellow:
Paul Hudak Hai (Paul) Liu
308 AKW 313 AKW
432-1235 432-1267
paul.hudak@yale.edu hai.liu@yale.edu
Office hours:
    Tue/Thu 2:30-3:30pm		 Office hours:
    Mon 3:00-5:00pm

Textbooks: 

There is one required textbook for the course:

	Theories of Programming Languages
	by John C. Reynolds
	Cambridge University Press, New York, 1998

This book should be available now at the Yale Bookstore.  This website also has copies of lecture slides for most of the chapters.  The textbook will also be supplemented with other material as needed.

For some parts of the course, we will use Haskell as a semantics prototyping language.  Haskell is a purely functional language that is quite a bit different from mainstream languages such as C, C++, or Java.  For the most part we will use only the most basic features of Haskell, but if you are unfamiliar with the language I would recommend reading a tutorial such as: A Gentle Introduction to Haskell found at: http://haskell.org/tutorial/, or you may find the following book useful:

	The Haskell School of Expression --
	Learning Functional Programming through Multimedia 
	by Paul Hudak
	Cambridge University Press, New York, 2000
	http://haskell.org/soe

Computing Resources:

The Haskell implementation that we will use is called GHC, and will be installed in the Department's educational computing cluster (the Zoo), which is located on the third floor of A.K. Watson Hall (the Computer Science Department, at 51 Prospect Street).  Please visit http://zoo.cs.yale.edu/cgi-bin/accounts.pl to register for this class in the Zoo, even if you already have an account in the Zoo.   By registering for the class, a work directory will be created for you in /home/classes/cs430/class.

If you prefer to run GHC on your own computer (laptop or otherwise), go to http://haskell.org/ghc where you will find instructions on how to download the system for either Windows or Linux machines.

Web Page and Newsgroup:

This web page (plucky.cs.yale.edu/cs430)  will the source of programming assignments, solutions, and other relevant information.  We will also be using Yale's "Classes" server, which is located at http://classesv2.yale.edu.  More on this at a later date.

Required Work:

There will be several problem sets and a take-home final exam (no mid-term).  The work will be graded by your TA and returned, along with solutions, nominally within one week.  Late work will be accepted at the discretion of the instructor and/or TA.  Assignments turned in after solutions have been published will not be accepted, even with a Dean's excuse, although alternative make-up work may be authorized.

It should go without saying that when you hand in (electronically or otherwise) a paper with your name on it, I assume that you are certifying that this is your work, and that you were involved in all aspects of it.  It is Ok to work with other students on the concepts underlying an assignment, but you are expected to do the actual assignment on your own, based on your own level of progress with the material.

Your grade will be based on a combination of homework assignments and the final exam.  You are expected to do all of the homework assignments, which will count as a significant part of your grade!