CS565: Programming Languages
TTh 10:30-11:45 |
Hybrid Delivery |
|
about
Instructor:
bendy at purdue.edu
Office Hours: Tuesday, 10:30a-12:00p, WebEx
Teaching Assistant:
Qianchuan Ye
ye202 at purdue.edu
Office Hours: Thursday 2:00-3:30, WebEx
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 fall's
offering of CS565 is structured so that it can
be taken entirely asynchronously:
Lectures:
There will be no in-person instruction this
semester. Each Monday, recorded lectures will be
posted on Brightspace. Students are expected to
watch these lectures during 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 the
week's quizzes by 5p on Friday.
Live Labs:
Each Thursday from 10:30-12:00, there will be
a live lab session in which the professor will
answer student questions (including those posted
to piazza), and interactively work through
example problems. These sessions will be
recorded and will be posted the following
day.
Office Hours:
Each Tuesday from 10:30-12:00, the
instructor will have virtual office hours. In
the event that students cannot attend these
virtual office hours, they should contact the
instructor via email to schedule a time to meet
individually.
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 TA 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. The latest version of Coq
is 8.12, which should be used 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 50% 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 20% and 30% of your final grade,
respectively. To summarize, final grades will be
assigned according to the following breakdown:
Homework Assignments |
40% |
Midterm (10/16) |
20% |
Final (12/09) |
30% |
Participation Quizzes |
10% |
|
(tentative) schedule
Date |
Topic |
Notes |
Homework |
08/24 |
Functional Programming in Coq
|
|
|
08/31 |
Polymorphism + Basic Reasoning
|
|
|
09/07 |
Inductive Evidence + PL Foundations |
|
|
09/14 |
Basic Operational Semantics |
|
|
09/21 |
Advanced Operational Semantics |
|
|
09/28 |
Untyped Lambda Calculus
|
|
|
10/05 |
Denotational Semantics |
|
|
10/12 |
Midterm Review / Midterm |
|
|
10/19 |
Axiomatic Semantics / Program Logics |
|
|
10/26 |
Advanced Program Logics |
|
|
11/02 |
Introduction to Type Systems |
|
|
11/09 |
Type Inference / Reconstruction |
|
|
11/16 |
Advanced Type Systems
| |
|
11/23 |
Flex Time / Advanced Topics |
|
|
11/30 |
Review for Final / Course Recap
|
|
|
12/07 |
Final Exam
Details TBD
|
|
|
|
|
|