CS 565: Programming Languages

Spring 2024

Meeting Time

Monday, Wednesday, Friday: 9:30 - 10:20
Grissom Hall 103

Instructor

Suresh Jagannathan
LWSN 3154J
Ph: x4-0971
email: suresh@cs.purdue.edu
Office Hours: Monday, Wednesday: 12pm - 1pm

Teaching Assistants

Pedro Da Costa Abreu
Wed. 11AM - 12pm, HAAS G072
email: pdacost@purdue.edu

Srinivasa Arun Yeragudipati
Tues. 2PM - 3PM, HAAS 143
email: syeragud@purdue.edu

Course Overview

The field of programming languages is as old as computing itself, and is central to the way we transform abstract algorithmic notions to concrete executable plans. While some aspects of language design entail issues related to choice of syntax (e.g., Lisp), contain features that are only relevant to the specific domains in which the language is intended to operate (e.g., XML), or are centered around particular methdologies the language designer wishes to promote (e.g., Javascript), much of the focus in the study of programming languages centers on more universal, foundational questions.

Rather than evaluating a programming language in terms of qualitative judgments (why is language X better to write programs in than language Y ?), we are interested in pursuing a more substantive line of inquiry centered around notions of semantics and correctness - what are the tools and methods that can be used to rigorously describe what a program does or means, without injecting subjective bias into our characterization; and, how do we ascertain from this description, assurance that any execution of this program will be faithful to the intent of the developer?

More generally, these questions broadly fall under the term formal methods, an important branch of Computer Science that allows us to precisely reason about programming language features and behaviors using logical principles. Our focus will be to explore core ideas in programming languages from this perspective. To do so, we will undertake our study using small language definitions (program calcuii), sufficiently expressive to serve as useful objects of study, but not burdened with features that, while necessary for practical use, are not semantically interesting.

The course will be centered on tools, techniques, and methodologies that enable better understanding of how we might design, specify, and implement various kinds of language features related to notions of state, modularity, and abstraction. We will also use these mechanisms to help us think about how to gain stronger assurance and confidence that the programs we write do what we expect them to do.

From the above description, you can conclude that this course will not be a survey of existing languages or a taxonomy of language constructs. Neither will it be a course on compilers or software engineering per se. While implementation principles will be discussed periodically, this will not be an important focus of the course. Instead, the material we present will be mostly intended to allow us to explore new ways to understand programming languages, helping us to answer questions such as the following:

  1. What is the meaning of a program specification and what role do specifications play in program construction and reliability?
  2. How do we verify that a program adheres to its specification?
  3. What are sensible and tractable notions of program correctness? What are the conditions under which we can assert that a program is “safe”?
  4. How do we prove useful properties about a program; what do we mean by a proof in this context?
  5. How do we qualify the “expressive power” of a language feature? How do we relate different features found in different languages?
  6. What is a type and how can they be used to reason about program correctness?
  7. How foundationally different are various methodologies espoused by different languages (e.g., object-oriented, functional, imperative)?
  8. How do we reason about the equivalence of programs, or programs and their compiled translation?
  9. What tools can we bring to bear to help automate the way we reason about a program’s behavior?

To help answer these questions, the course is designed around several interleaved themes: (1) the role of logic and related mathematical formalisms to enable writing rigorous specifications of a program's behavior; (2) formal reasoning devices that explain the meaning (or semantics) of programming language features and program executions; (3) the use of types to define and specify safety conditions on program executions, and to enrich language expressivity; (4) characterization of different notions of correctness and development of mechanisms to verify that programs are correct with respect to their specification; (5) the use of automated tools (e.g., proof assistants, program verifiers) to help validate important theorems that describe useful program properties.

By the end of the class, students should be comfortable with objectively assessing and comparing superficially disparate language features, understanding how these features impact implementations, be able to distinguish concepts that are truly foundational from those that just appear to be, and be able to critically reason about program correctness and safety. Most importantly, the overarching goal of this course is to equip students to ask better questions about language design, even if the answers themselves are not readily apparent.

Prerequistes

It is assumed that students taking this class have had exposure to programming at the undergraduate level, and are comfortable with basic mathematical concepts (e.g., sets, functions, relations, basic rules of logic), and software implementation techniques. There will be a number of programming exercises in the class, using proof assistants (Coq) and automated verification tools (Dafny) but no prior background in any specific programming language is necessary.

Academic Honesty and Collaboration

Students are encouraged to work together to clarify issues presented in class. However, students are not allowed to collaborate on programming assignments or examinations. We will use Piazza for posting and answering questions about lectures, homeworks, etc.

Grading

Grading for the class is as follows:

  1. Homeworks: 35%
    There will be regular homework exercises; there are 7 planned over the course of the semester. Each exercise will consist of some number of recommended problems that you can use to guage whether have understood the basic concepts of the material covered by the exercise, and some number of required problems that test how well you have assimilated these concepts by applying them in situations different from what we examine in class. Answers will be provided for both classes of problems, but you will only be graded on your submission to the required problems.

  2. Quizzes: 10%
    There will be weekly take-home quizzes. These quizzes will consist of 3 - 5 multiple-choice or short-answer questions posted on Gradescope. These quizzes are intended to test your understanding of lecture material covered in class.

  3. Midterm: 25%
    The midterm will be an evening exam scheduled for Wednesday, March 20, 2024, 8:00pm - 9:30pm, KRAN G016

  4. Final (Cumulative): 35%
  5. The final will be take home. While you are encouraged to discuss the material with your classmates, and post questions on Piazza, it is expected that homework submissions and exams reflect the work of the student alone.

Text and Resources

We will use the online textbook Software Foundations, available here for part of the course. Students should download the text, and install the Coq mechanized proof assistant (see here). There are a number of IDEs available for Coq: CoqIde (available as part of the Coq download), or Proof General, a Coq IDE for Emacs users are two popular choices. For those of you who decide to use Proof General, Company Coq provides additional syntax highlighting and auto complete features. The textbook is essentially one large Coq program, with explanation provided in comments, so students are encouraged to bring their laptops to class to interactively explore the material during the lecture. There is extensive documentation for Coq; see here for the reference manual and here for a list of available tactics.

In addition, students might find the following texts also useful:


The latter half of the course will also use Dafny, an automated verification-aware programming language. Material for this part of the course will be adapted from the textbook, Program Proofs (available here). As with Coq, you will also need to install Dafny, along with your preferred form of IDE support. The installation instructions provide several alternatives.

Topics

The course is roughly divided into the following topic areas that will be covered more-or-less in the order given below.

Foundations

Semantics

Types

Automated Program Verification

Lectures

January 8 - 12, 2024

  Topics: Course Introduction, Functional Programming, Inductive Datatypes
  1. Readings: Basics
  2. Lecture slides
  3. HW: Setup: Download and install Coq and Dafny.
January 15 - January 19, 2024

  Topics: Induction
  1. Readings: Induction
  2. Lecture slides
  3. Homework 1: Due: January 29, 2024 (updated)
January 22 - January 26, 2024

  Topics: Lists, Polymorphism
  1. Readings: Lists, Polymorphism
  2. Lecture slides
January 29 - February 2, 2024

  Topics: Logic, Inductively-Defined Propositions
  1. Readings: Logic, Inductive Propositions, Tactics and Automation
  2. Lecture slides
  3. Homework 2: Due: February 9, 2024
February 5 - February 9, 2024

  Topics: Relations, Proof Objects
  1. Readings: Relations, Curry-Howard Isomorphism, Induction Principles
  2. Lecture slides
February 12 - February 16, 2024

  Topics: A Simple Imperative Language, Program Equivalences
  1. Readings: A Simple Imperative Language, Program Equivalence,
  2. Lecture slides
  3. Homework 3: Due: February 23, 2024
February 19 - February 23, 2024

  Topics: Operational Semantics
  1. Readings: Smallstep Operational Semantics
  2. Lecture slides
February 26 - March 1, 2024

  Topics: Type Systems
  1. Readings: Introduction to Type Systems Simply-Typed Lambda Calculus Properties
  2. Lecture slides
  3. Homework 4: Due: March 8, 2024
March 4 - March 8, 2024

  Topics: Subtyping, System F
  1. Readings: More STLC, Subtyping
  2. Lecture slides
March 11 - March 15, 2024

   Spring Break

March 18 - March 22, 2024

  Topics: Hoare Logic
  1. Readings: Hoare Logic (Part 1), Hoare Logic (Part 2)
  2. Lecture slides
  3. Homework 5: Due: March 29, 2024 Midterm: Wednesday, March 20, 8-9:30PM, KRAN G016
    No class: Friday, March 22nd
March 25 - March 29, 2024

  Topics: Introduction to Dafny
  1. Readings: Chapter 1, Program Proofs
  2. Lecture slides
April 1 - April 5, 2024

  Topics:Weakest Preconditions, Strongest Postconditions
  1. Readings: Chapters 2: Program Proofs
  2. Lecture slides
  3. Homework 6: Due: April 12, 2024
April 8 - April 12, 2024

  Topics: More Complex Specifications, Dealing with Loops
  1. Readings: Chapters 5, 11: Program Proofs
  2. Lecture slides
April 15 - April 19, 2024

  Topics: Arrays and Searching
  1. Readings: Chapters 13, 14: Program Proofs
  2. Lecture slides
  3. Homework 7: Due: April 26, 2024