Tuesday, Thursday: 3:00 - 4:15
BHEE 236
Suresh Jagannathan
LWSN 3154J
Ph: x4-0971
email: suresh@cs.purdue.edu
Office Hours: Tuesday, Thursday: 12pm - 1pm
Anmol Sahoo
sahoo9@purdue.edu
Office Hours: TBD
This course studies the design
of programming languages, not by examining its syntax or how it's
implemented, but from a more foundational perspective that focusses
the \emph{semantics} or meaning of the constructs the language
defines and the way these constructs interact with each other.
Rather than trying to understand programming languages in terms
of qualitative judgments (why is
language X better to write
programs in than
language Y?), we'll pursue
a more substantive line of inquiry centered around the notion
of language calculii - 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 using the vocabulary provided by these abstractions, without
injecting subjective, qualitiative bias into our characterization; how do we
gain assurance from this description that any execution of
this program will be faithful to the developer's intent?
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,
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:
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) mechanisms that enable the formal description 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 to help validate that a program is correct.
By the end of the class, students should be comfortable with objectively assessing and comparing
superficially disparate language features, understanding how these features impact usability and expressivity, 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.
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 adn Dafny but it is not expected that
students would have experience with them prior to this class.
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:
There is no required textbook
for the class, but you might find the material in the following to
be useful:
Foundations
Semantics
Program Verification
Prerequistes
Academic Honesty and Collaboration
Grading
There will be regular homework exercises; there are 7
planned over the course of the semester. One class of homework
involve implementing (using OCaml)
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 second 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.
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.
Weekly (autograded) quizzes will be posted on Gradescope that will exercise your
understanding of material covered in the lectures.
There will be an in-class midterm held on Thursday, October 16, 2025.
Text and Resources
Programming exercises will be written in OCaml and
Dafny.
OCaml is a mature language with excellent IDE support, including plug-ins for
Visual Studio
and
Emacs.
There are many
resources available for learning OCaml, some of which are listed below:
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.