CS 456: Programming Languages

Fall 2024

Meeting Time

Tuesday, Thursday: 3:00 - 4:15
BHEE 236

Instructor

Suresh Jagannathan
LWSN 3154J
Ph: x4-0971
email: suresh@cs.purdue.edu
Office Hours: Tuesday, Thursday: 11am - 12pm

UTA

Priyam Gupta
email: gupta751@purdue.edu
Office Hours: Monday: 3pm - 4pm

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 Cuda), or are centered around particular methdologies the language designer wishes to promote (e.g., object-oriented programming), 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 the notion of language semantics - how can we define a core set of abstractions for expressing a rich class of data and control mechanisms; what are the tools and methods that can be used to rigorously describe what a program means, without injecting subjective bias into our characterization; 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, mathematically-grounded, 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 important features found in modern programming languages. We will also use these mechanisms to help us think about how to gain stronger assurance and confidence that the programs we write behave the way we expect.

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. How can we "grow" a language from a small core of data and control abstractions to express existing mechanisms found in modern real-world languages? What are the building blocks for control and data abstractions?
  2. What is the meaning of a program specification and what role do specifications play in program construction and reliability?
  3. What is a type and how can they be used to reason about program correctness?
  4. How do we verify that a program adheres to its specification?
  5. How do we qualify the “expressive power” of a language feature? How do we relate different features found in different languages?
  6. How foundationally different are various methodologies espoused by different languages (e.g., object-oriented, functional, imperative)?
  7. How do we reason about the equivalence of programs, or programs and their compiled translation?
  8. 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 development of program calculii (e.g., lambda calculus) as a convenient means to explore diffeent language features; (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., solver-aided languages) 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 reason about how to establish the correctness and safety of the programs they write. 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. It is not required that they have previously taken a course in compiler design. There will be a number of programming exercises in the class using OCaml and Dafny but it is not expected that students would have experience in programming with these languages prior to this class.

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 8 planned over the course of the semester. These will be either programming exercises (approximately 6) in which you will implement interpreters for a simple core language. The language and/or implementation technique used by the interpreter will differ across homeworks, but the expectation is that insights gleaned from previous homeworks will be applicable to later ones. The remaining assignments will be program verification exercises in which you will use a state-of-the-art program verifier (Dafny) to validate that a program adheres to its provided specification.

    Students will self-grade their assignment. Along with the implementation, you will also submit a detailed assssment summary that (i) summarizes your solution; (ii) provides an explanation of how you validated the correctness of your solution (e.g., the test cases used, the number of tests that succeeded or failed, etc.); (iii) a discussion on the limitations of your solution; and (iv) a summary of the insights that you gleaned from the exercise.

  2. Quizzes: 5%
    (Mostly) weekly (autograded) quizzes will be posted on Gradescope that will exercise your understanding of material covered in the lectures.

  3. Midterm: 25%
    There will be an in-class midterm held on Thursday, October 17, 2024.

  4. Final (Cumulative): 35%
  5. There will be a cumulative final held during finals week.

Text and Resources

There is no required textbook for the class, but you might find the material in the following to be useful:


Programming exercises will be written in OCaml and Dafny. There are many resources available for learning OCaml, some of which are listed below:
OCaml is a mature language with excellent IDE support, including plug-ins for Visual Studio and Emacs.

Dafny is an automated verification-aware programming language. Material for those parts of the course that use Dafny will be adapted from the textbook, Program Proofs (available here). The installation instructions provide several alternatives for IDEs that you can use to interact with Dafny.

Topics

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

Foundations

Semantics

Program Verification

Lectures

August 20 - August 22, 2024

  Topics: Course Introduction and Overview, OCaml, Functional Programming, Datatypes
August 27 - August 29, 2024

  Topics: Lambda Calculus, Evaluation Strategies
September 3 - September 5, 2024

  Topics: Fixpoints, Recursion, Continuations, A-Normal Form
September 10 - September 12, 2024

  Topics: Introduction to Types, Simply-Typed Lambda Calculus
September 17 - September 19, 2024

  Topics: System F, Parametric Polymorphism
September 24 - September 26, 2024

  Topics: Type Inference
October 1 - October 3, 2024

  Topics: Subtyping
October 8 - October 10, 2024

  Topics: Reasoning about State, Monads
October 15 - October 17, 2024

  Topics: Monads (cont), Midterm Review
October 22 - October 24, 2024

  Topics: Introduction to Semantics, IMP
October 29 - October 31, 2024

  Topics: Smallstep and Denotational Semantics
November 5 - November 7, 2024

  Topics: Axiomatic Semantics, Hoare Logic
November 12 - November 14, 2024

  Topics: Introduction to Dafny
November 19 - November 21, 2024

  Topics: Proof Principles
November 26 - November 28, 2024

  No class (Thanksgiving break)

December 3 - December 5, 2024

  Topics: Course Review
  No class December 5