Tuesday, Thursday: 3:00 - 4:15
BHEE 236
Suresh Jagannathan
LWSN 3154J
Ph: x4-0971
email: suresh@cs.purdue.edu
Office Hours: Tuesday, Thursday: 11am - 12pm
Priyam Gupta
email: gupta751@purdue.edu
Office Hours: Monday: 3pm - 4pm
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. 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:
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.
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.
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
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?
Prerequistes
Academic Honesty and Collaboration
Grading
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.
(Mostly) 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 17, 2024.
Text and Resources
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.