about

Instructor:

Ben Delaware

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

COVID-19 Impact

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:

1. principles (e.g., semantics, type systems, specifications)
2. proof techniques and formal reasoning
3. 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:

1. Programming in an imperative language, e.g. Java / C / Python, etc.
2. 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.
3. 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:

(tentative) schedule