Tuesday, Thursday: 12:00 - 1:15

LWSN B155

Suresh Jagannathan

LWSN 3154J

Ph: x4-0971

email: suresh@cs.purdue.edu

Office Hours: Tuesday, Thursday: 2 - 3pm

Agresh Bharadwaj

Time: Wednesday 12pm - 1pm

Zoom Meeting Room ID : 399 465 7406

email: bharad14@purdue.edu

Songlin Jia

Time: Monday 6pm - 7pm

Location: HAAS G050

Zoom Meeting Room ID : 920 221 6025

email: jia137@purdue.edu

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., Cuda), or are centered around particular methdologies the language designer wishes to promote (e.g., Javascript), other aspects of the study of programming languages are more universal, concerned with exploring foundational questions. That is, beyond thinking of programming languages in terms of qualitative judgments (why is language X better to write programs in than language Y ?), we might pursue a more substantive line of inquiry centered around notions of semantics and correctness - how can we best 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? Surprisingly, answers to these questions can often be pursued without appealing to specific syntactic forms or any particular design features.

More generally, these questions broadly fall under the term *formal methods*, an important branch of
computer science that looks to mathematics (specifically, logic) to help us (at least in this class) precisely
reason about programming language features and behaviors. Our focus will be to explore core ideas in
programming languages from a rigorous, foundational, and principled perspective enabled by couching
programming language concepts and the vocabulary we use to reason about them in terms of
well-defined mathematical objects (e.g., sets, functions, relations) and associated reasoning
strategies (e.g., induction). To do so, we will undertake our study using small language definitions
(program calcuii), sufficiently expressive to serve as a useful object of study, but not burdened
with features that while perhaps necessary for real-world implementations, are semantically
uninteresting.

The course will be centered around the use of tools (proof assistants, model checkers, type systems) that enable better understanding of how we might design, specify, and implement language features. We will also use these tools 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 programming or software
engineering *per se*. Instead, presented material will be structured to allow us to explore new ways to
understand programming languages generally that help us to answer questions such as the
following:

- What is a program specification and what role do specifications play in program construction and reliability?
- What does program verification mean?
- What are sensible and tractable notions of program correctness? What are the conditions under which we can assert that a program is “safe”?
- How do we prove useful properties about a program; what do we mean by a proof in this context?
- How do we qualify the “expressive power” of a language feature? How do we relate different features found in different languages?
- What is a type and how can they be used to reason about program correctness?
- How foundationally different are various methodologies espoused by different languages (e.g., object-oriented, functional, imperative)?
- How do we reason about the equivalence of programs, or programs and their compiled translation?
- 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 in programming language specification and design; (2) formal reasoning devices that precisely explain the meaning 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 properties based on the structure of (2) and (3), using techniques enabled by (1).

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.

It is assumed that students taking this class have had exposure to programming at the undergraduate level, and are comfortable with basic mathematical concepts, 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.

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 for the class is as follows:

**Homeworks**: 30%

There will be regular homework exercises, roughly 6 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. While there is no partial credit for homeworks, a good-faith submission, regardless of the number of correct responses, puts a floor at 50%.

**Midterm**: 30%**Final (Cumulative)**: 40%
Both the midterm and 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.

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:

- Certified Programming with Dependent Types, Adam Chlipala, MIT Press, 2013
- Types and Programming Languages, Benjamin Pierce, MIT Press, 2002.

*Foundations*

- Functional Programming
- Induction Principles
- Logic and Propositions
- Curry-Howard Correspondence
- Relations

*Specifications, Semantics, and Verification*

- Program Equivalence
- Operational Semantics
- Hoare Logic
- Separation Logic
- Automated Program Verification

*Types*

- Simply-Typed Lambda Calculus
- Polymorphism
- Subtyping
- Advanced Topics

- Lists
- Polymorphism
**Homework 1**: Due: September 8, 2022

- Inductive Propositions
**Homework 2**: Due: September 23, 2022

- A Simple Imperative Language
- Program Equivalence
**Homework 3**: Due: October 6, 2022

- Hoare Logic
- Hoare Logic (cont)
**Homework 4**: Due: October 27, 2022

- Examples
**Homework 5**: Due: November 10, 2022

- Simply-Typed Lambda Calculus
- Properties of STLC
**Homework 6**: Due: November 29, 2022