CS 565: Programming Languages

Handout 1:                                                                       August 2011

Instructor Prof. Suresh Jagannathan Room 3154J Lawson Ph: x4-0971 Email: suresh@cs.purdue.edu Office Hours: Tu, Th. 2 - 3PM

Teaching Assistant Siddharth Tiwary Room 3133 Lawson Ph: 49-69405 Email: stiwary@cs.purdue.edu Office Hours: M,W . 2 - 3PM

Syllabus

This course will examine the design and implementation of programming languages from a foundational perspective.  Our goal will be to develop tools that will enable us to both design and specify new language features, to precisely understand the rationale for existing features in modern languages, and to understand how design decisions can impact implementations.  The course will be divided into roughly three parts: (1) principles (e.g., semantics, type systems, specifications); (2) proof techniques and formal reasoning and (3) automated theorem proving using the Coq proof assistant.   Our discussion of principles will be crafted in the context of definitions and theorems that capture salient properties of modern languages. The validation of these theorems will be undertaken using Coq, a powerful theorem prover and mechanized proof assistant.

A detailed syllabus can be found here.

Newsgroup and Message Boards

We will be using piazza as the main newsgroup and message board for the course. Piazza allows students and instructors to post and collaboratively answer questions or address issues pertaining to the course.

Lectures

Lecture 1:   Introduction and Course Overview.

Lecture 2:   Operational Semantics.

Software Foundations

Table of Contents


SfLib.v

Preface.{ html, v }
Basics.{ html, v }
Lists.{ html, v }
Poly.{ html, v }
Prop.{ html, v }
Logic.{ html, v }
Imp.{ html, v }
ImpList.{ html, v }
Hoare.{ html, v }
HoareAsLogic.{ html, v }
SmallStep.{ html, v }
Types.{ html, v }
Stlc.{ html, v }
MoreStlc.{ html, v }
Subtyping.{ html, v }

Homework

Homework 1. Due: August 29, 2011.
   Name your file hw1.v. Then, use the following on any departmental machine to submit: turnin -c cs565 -p project1 hw1.v

Homework 2. Due: September 5, 2011.
   Name your file hw2.v. Then, use the following on any departmental machine to submit: turnin -c cs565 -p project2 hw2.v

Homework 3. Due: September 19, 2011.
   Name your file hw3.v. Then, use the following on any departmental machine to submit: turnin -c cs565 -p project3 hw3.v

Homework 4. Due: September 26, 2011.
   Name your file hw4.v. Then, use the following on any departmental machine to submit: turnin -c cs565 -p project4 hw4.v

Homework 5. Due: October 10, 2011.
   Name your file hw5.v. Then, use the following on any departmental machine to submit: turnin -c cs565 -p project5 hw5.v

Homework 6. Due: October 24, 2011.
   Name your file hw6.v. Then, use the following on any departmental machine to submit: turnin -c cs565 -p project6 hw6.v

Homework 7. Due: October 31, 2011.
   Name your file hw7.v. Then, use the following on any departmental machine to submit: turnin -c cs565 -p project7 hw7.v

Homework 8. Due: November 13, 2011.
   Name your file hw8.v. Then, use the following on any departmental machine to submit: turnin -c cs565 -p project8 hw8.v

Homework 9. Due: November 28, 2011.
   Name your file hw9.v. Then, use the following on any departmental machine to submit: turnin -c cs565 -p project9 hw9.v

Sample Final is here.