CIS 5000: Syllabus

Overview:

This course introduces basic concepts and techniques in the foundational study of programming languages, as well as their formal logical underpinnings. The central theme is the view of individual programs and whole languages as mathematical objects about which precise claims may be made and proved. Particular topics include operational techniques for formal definition of language features, type systems and type safety properties, polymorphism and subtyping, and foundations of advanced programming-language features.

Topics:

Part I: Logical Foundations

Functional programming

Constructive logic

Inductive definitions and proof techniques for informal and formal proof

The Rocq proof assistant

Part II: Programming Language Basics

Operational semantics

Semantics of the imperative While language

Part III: Type systems

Simply typed λ-calculus

Type safety

Subtyping

Textbook:

Online textbooks: Logical Foundations and Programming Language Foundations

Supplementary textbook: Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.

Prerequisites:

An undergraduate-level course in programming languages or compilers; significant programming experience; mathematical sophistication.

Grading:

Breakdown for the course grade is as follows:

• Homework: 25%
• Quizzes: 5%
• Midterm 1: 20%
• Midterm 2: 20%
• Final Exam: 30%

Homework

Working with the CIS 5000 Rocq Projects

• CIS 5000 has many homework assignments that build on each other. Keeping current with the course material is extremely important for successfully completing the course.

• Each assignment consists of a few Rocq *.v files that you will modify and submit for grading. Further instructions will be provided along with the homework announcements, and you can find additional documentation about setting up your project environment in the Preface of the textbook.

Submission Policy

When submitting Rocq files as homeworks, make sure that Rocq accepts each file in its entirety. If Rocq does not accept the file, it will not be graded. You can use Admitted to force Rocq to accept incomplete proofs (but you will not get credit for those problems).

Late Submission Policy

The late submission policy is intended to encourage students to complete every homework to the best of their ability while still allowing them a bit of flexibility throughout the semester to account for scheduling challenges. If you have unusual circumstances please contact the instructor.

• Any homework submitted before the due date is considered on time.

• Any homework submitted after the due date is considered late. The difference between the submission time and the due date is the number of hours the assignment is overdue.

• In the absence of unusual circumstances, homework cannot be submitted after 48 hours past the due date. (We will close the submission site at that time.)

• For each 24 hours overdue (or fraction thereof) that a homework is submitted late, the student accrues one "late day". "Late days" are atomic, indivisible units, partial late days are not permitted.

• Any homework that is not submitted at all will receive a score of 0 and cause the student to accrue 2 late days.

• Accrued late days do not impact any individual homework score. Instead, they apply to the final weighted, letter grade of the class, as follows:

  • 0 - 8 late days: no grade penalty
  • 9 - 16 late days: one-third letter grade penalty (A becomes A-, A- becomes B+, B+ becomes B, etc.)
  • 17 - 20 two-thirds letter grade penalty (A becomes B+, A- becomes B, B+ becomes B-, etc.
  • 21 - 24 late days: one full grade penalty (A becomes B, A- becomes B-, B+ becomes C+, etc.)

• Students do not have to notify the course staff about late submissions.

• Students should be able to calculate the number of late days they have accrued by looking at the information on the homework submission site. However, any student wishing to know the total number of late days that they have accrued should contact the course staff.

Unusual Circumstances

If you have unusual medical, family, or other emergency circumstances, please contact the instructor as soon as possible so that an appropriate plan for completing the course material can be created. It is preferable that you contact the course staff before the homework due date or exam, in which case we will do our best to accommodate the unusal circumstances. If you do not contact the staff in advance, it is up to the instructor's discretion whether a late assignment falls into the unusual circumstances category, or whether it causes the student to accrue late days.