CS565: Programming Languages
|
about
Instructor:
bendy at purdue.edu
Office Hours: Tuesday, 3:30p-5:00p, LWSN 2116M
Teaching Assistants:
Pedro da Costa Abreu
Email: pdacost at purdue.edu
Office Hours: Wednesday, 4:00p-5:30p, HAAS 175
Nitin Raj
Email: rajn at purdue.edu
Office Hours: Monday, 11:30a-1:00p, HAAS 175
Reflecting the unfortunate realities of the
ongoing COVID-19 pandemic, this spring's
offering of CS565 is structured so that all
its materials can be
accessed online.
The information on this webpage reflects the
current plan for the course, and
its format may be
changed to adapt to pandemic-related
developments.
In the interest of providing students with a
unified dashboard for all their classes, we
will be
using Brightspace
as the main repository for course content
including lectures, homeworks, and
announcements.
Course Description:
This course will examine the design and
implementation of programming languages from a
foundational perspective. Our goal will be to
develop tools that will enable us to both design
and specify new language features, to precisely
understand the rationale for existing features in
modern languages, and to understand how design
decisions can impact implementations. The course
will be divided into roughly three parts:
-
principles (e.g., semantics, type systems, specifications)
-
proof techniques and formal reasoning
-
interactive theorem proving using the Coq proof assistant
Our discussion of principles will be crafted
in the context of definitions and theorems
that capture salient properties of modern
languages. The validation of these theorems
will be undertaken using Coq, a powerful
theorem prover and mechanized proof assistant.
Course-Level Learning Outcomes:
At the end of this course, students will be able to:
- Compare and contrast different approaches to specifying a programming language's behaviors (and how they effect reasoning about programs).
- Specify different categories of program errors and apply language-based techniques to ensure their absence. In particular, students will learn about the theory and practice of:
- Program logics,
- and Type Systems
- Rigorously formalize and reason about systems in the Coq proof assistant. In particular, students will be able to:
- define mathematical representations of systems,
- state their properties in logic,
- and formally prove those properties hold.
|
logistics
Reflecting the unfortunate realities of the
ongoing COVID-19 pandemic, this spring's
offering of CS565 is structured so that all
its materials can be accessed online:
Lectures:
In-class instruction will be a mixture of of
lectures and live labs. After each lecture, a
recorded version will be posted on
Brightspace. Students that miss class are
expected to watch these lectures within the week
they are posted and post any questions they have
to the course discussion board.
Participation Quizzes:
Each lecture will be accompanied by a brief
quiz that will also posted on
Brightspace. Students are expected to finish a
lecture's quizzes within the next seven
days. Quizzes close at 5:00p.
Live Labs:
During live lab sessions, the professor will
answer student questions (including those posted
to piazza), and interactively work through
example problems.
Homeworks:
Homeworks will be posted every other week
according to the course schedule. These
assignments will require students to fill in
missing definitions and proofs in an incomplete
Coq file. Homeworks are to be submitted via
Brightspace by 6PM on their assigned due
date. Make sure that Coq accepts your file in
its entirety. If it does not, it will not be
graded. You can use Admitted to force Coq to
accept incomplete proofs. Everyone will receive
three courtesy late days for the semester. Once
all these days have been used, students will
need to notify the instructor or the TA ahead of
time with an explanation and plan for
completion. These requests will be accepted at
my discretion and may include a point penalty of
5% per day late. Asking for an extension does
not guarantee it will be granted.
|
success
How to Succeed in this Course
In order to be successful, students should be familiar with:
- Programming in an imperative language, e.g. Java / C / Python, etc.
- Basic logic and proofs techniques found in an undergraduate discrete math course like CS182: sets, relations, functions, proof by induction, proof by case analysis; recursion; and propositional logic.
- The sorts of basic data structures and algorithms encountered in an undergraduate course like CS 251, e.g. lists, trees, heaps, graphs, sorting, graph traversals, and search.
We'll briefly review important concepts as needed, but this will be a refresher and not an introduction.
In this course, we will be using the Coq proof
assistant as a sort of 'personal TA' to check
our work. As you work through homework In this
course, we will be using the Coq proof
assistant as a sort of 'personal TA' to check
our work. As you work through homework
assignments, Coq will identify any gaps in
your reasoning and provide immediate
feedback. Once Coq gives the thumbs up on a
homework problem, you can be reasonably
confident that you have finished it correctly
correct. This tight feedback loop can lead to
an unfortunate anti-pattern, however, in which
students blindly push buttons until they
happen upon something that works. This
approach will waste a lot of your time and
will not help you learn the material. Students
should resist the temptation to immediately
start hacking on a problem in Coq, and instead
work out a solution on pen and paper. Only
once you have found a should you code it up in
Coq, relying on the proof assistant to check
your reasoning.
|
resources
Course Text:
We will be
using
Software Foundations as the course
textbook.
Types and Programming Languages has a
more in-depth treatment of semantics and type
systems,
while
Certified Programming with Dependent
Types is an excellent resource for
applied programming and proving in Coq.
Discussion Forum:
The
course piazza
site will serve as the discussion board; all
course announcements will also be posted
there. In lieu of emailing the instructor or
the TAs with any general questions about using
Coq or assignments, please post them to piazza
so that any other students with the same
question can see the answer.
Coq:
The official
project
page of the Coq proof assistant has
plenty
of
documentation. Students should use version
8.12 or greater for all assignments.
|
policies
Assessment:
Students will be assessed through a
combination of biweekly homeworks, a midterm,
and a final exam. Due to the pandemic, both
the midterm and the final will be take
home. Details on the assignments and exams,
including a schedule of due dates, will be
posted to Brightspace.
Grading Structure:
Final grades in this course will reflect the
sum of your achievement throughout the
semester. Homework assignments are worth 60% of
your final grade, and each assignment will
contribute equally to your final homework
grade. Both the midterm and final will be
cumulative, although the final focusing more on
material from the second half of the
semester. The midterm and the final will be
worth 10% and 20% of your final grade,
respectively. To summarize how each kind of
assessment will be weighted:
Homework Assignments |
60% |
Midterm (03/07) |
10% |
Final (05/03) |
20% |
Participation Quizzes |
10% |
|
(tentative) schedule
Date |
Topic |
Notes |
Homework |
01/10 |
Functional Programming in Coq
|
|
HW 1 Assigned |
01/17 |
Polymorphism + Basic Reasoning
|
|
HW 1 Due (1/21) |
01/24 |
Inductive Evidence + PL Foundations |
|
HW 2 Assigned |
01/31 |
Basic Operational Semantics |
|
HW 2 Due (2/4) |
02/07 |
Advanced Operational Semantics |
|
HW 3 Assigned |
02/14 |
Modelling OO Languages |
|
HW 3 Assigned |
02/21 |
Untyped Lambda Calculus
|
|
HW3 Due (2/25) |
02/28 |
Denotational Semantics |
|
Practice Midterm Released |
03/07 |
Midterm Review / Midterm |
|
HW4 Assigned |
03/14 |
Spring Break |
|
|
03/21 |
Axiomatic Semantics / Program Logics |
|
|
03/28 |
Advanced Program Logics |
|
HW4 Due (04/01) |
04/04 |
Introduction to Type Systems |
|
HW5 Assigned |
04/11 |
Type Inference / Reconstruction |
|
HW5 Due (04/15) |
04/18 |
Formalizing Polymorphism / System F
|
|
HW6 Assigned |
04/25 |
Flex Time (Substructural Type Systems) / Course Wrapup
|
|
HW6 Due (4/21)
Practice Final Released |
05/02 |
Final Exam
Details TBD
|
|
|
|
|
|