Principles of Programming Languages

Comp Sci 704, Fall 2024

Schedule

This schedule is tentative and subject to change.

Date Topic Notes Assignment
Sept 4 Welcome + Course Overview [Syllabus] [Slides]
Optional: Useful background material
OCaml Programming: Correct + Efficient + Beautiful
Michael R. Clarkson
Core Topics
Sept 6 Preliminaries and Semantics [Notes]
Sept 9 Inductive Definitions and Operational Semantics [Notes]
Sept 11 Structural Induction [Same Notes]
Sept 13 Well-Founded Induction [Notes]
Sept 16 The IMP Language [Notes]
Sept 18 Class Cancelled (Ethan sick)
Sept 20 Big-step Semantics [Notes] HW1 Out
Sept 23 Denotational Semantics [Notes]
Sept 25 Axiomatic Semantics and Hoare Logic [Notes]
Sept 27 Predicate Transformers [Same Notes]
Sept 30 Class Cancelled (Ethan traveling)
Oct 2 λ-calculus [Notes]
Oct 4 λ-calculus Encodings [Notes]
Oct 7 Reduction Strategies and Evaluation Contexts [Notes] HW1 Due
Oct 9 Semantics by Translation
Oct 11 Observational Equivalence [Notes] HW2 Out
Oct 14 Recursive Functions [Notes]
Oct 16 Functional Language [Notes]
Oct 18 Functional Language (recursion) [Same Notes]
Oct 21 Scope [Notes]
Oct 23 State [Notes]
Oct 25 Continuations [Notes] HW2 Due / Midterm available
Oct 28 Exceptions [Notes]
Oct 30 Typed λ-calculus [Notes]
Nov 1 Products, Sums, and Datatypes [Notes] Midterm Due
Nov 4 Type Inference [Notes]
Nov 6 Subtyping [Notes] HW3 Out
Nov 8 Recursive Types [Notes]
Nov 11 Polymorphism [Notes]
Nov 13 Existential Types
Nov 15 Propositions as Types and Curry–Howard
Nov 18 Logical Relations and Normalization [Notes]
Special Topics
Nov 20 Information Flow Control and Noninterference
Nov 22 Class Cancelled (Ethan at Midwest PL Summit) HW3 Due
Nov 25 Enforcing Noninterference
Nov 27 No Class (Thanksgiving)
Nov 29 No Class (Thanksgiving)
Dec 2 Secure Downgrading
Dec 4 Abstract Interpretation
Dec 6 More Abstract Interpretation Final available
Dec 9 (TBD)
Dec 11 Wrap-up Final Due

Syllabus

(A pdf version of this syllabus is available here.)

Learning Outcomes

By the end of the course, you will be able to:

  • Define common programming language features using formal mathematical models, such as inference rules or denotational semantics.
  • State and prove theorems about the syntax, semantics, and type systems of programming languages using a variety of techniques, such as structural induction.
  • Analyze programming language properties, such as secure information flow or termination, using formal techniques such as type systems and abstract interpretation.

Course Communication

We will be using Piazza for course discussion. You can get to it through canvas. We encourage you to ask questions when you're struggling to understand a concept. It is also a good resource to find homework and study groups.

Please answer other students' questions if you know the answers. Course staff will give other students (at least) 24 hours to answer questions about concepts and material covered in the course before we provide an answer.

Assignments

The assignments in this course will consist of problem sets and exams, all handed in on Canvas.

Problem Sets

Problem sets will ask you to new things that you have not already practiced during lecture. This can make the homework feel difficult, and you may even get totally stumped on some problems. This is normal. But it does mean that you should start early and leave time to ask questions.

Problem sets are structured this way to for two reasons. First, exploring new ideas using existing concepts helps build and reinforce a deeper understanding and comfort with the material. Second, it allows me to assess your understanding as the course progresses and make adjustments as necessary.

Learning is often more effective (and more fun) as a collaborative activity. You are encouraged to work in groups on the problem sets.

Exams

Exams are designed to evaluate your abilities and fluency with the material. These problems will feel more familiar and should stretch you less. They will not, however, be slightly tweaked versions of problems from in class or homeworks.

Grading

Grades will be based on the following breakdown:

  • Problem sets: 45%
  • Midterm exam: 25%
  • Final exam: 25%
  • Participation: 5%

This is a graduate-level course. As such, the expectations are a bit different from what you may be used to in undergraduate-level courses. The focus of this course is on exposing you to new ideas and concepts and allowing you space to investigate and learn. Final grades will be curved.

Problem sets

Problem sets will be graded on a "✓" / "✓+" scale.

If you engaged with the material and did everything reasonably well, even if there were lots of mistakes, you will receive a ✓. This is the normal case.
✓+ If you did something surprisingly awesome, you will receive a ✓+. This is uncommon.
Note: This is essentially extra credit. Getting a ✓ on every homework is full credit.
0 If your work has major gaps, significant misunderstandings, or shows no engagement with the material, you will receive no credit. This is also uncommon.
Exams

Exams will receive a more standard point grade, and grading will be very nitpicky. We will give more weight to "small" mistakes and less to getting the right idea. This is the nature of this course, which is about mathematical formalism. Often, the intuitive idea behind a problem is very simple! Then, the topic we're working on is 100% about getting the nitty-gritty formal details right so we can prove something beyond a shadow of a doubt.

Remember, the goal is to demonstrate understanding. If you do not solve a problem completely, providing a partial solution along with an explanation of what is missing any why the solution does not entirely work can still get most of the points.

Participation

Participation grades will be based on two components:

  1. Stop by Ethan's office in the first two weeks of class to introduce yourself. Please come during office hours if you can, or contact Ethan to schedule another time if that is not possible.
  2. Active participation in class. This includes asking questions, answering questions, raising ideas, etc. This will be a very small portion of the grade.
A message for PhD students

Please try not to worry about your grade. I don't know how to put this delicately, but grades matter less as a PhD student than they did in undergrad. Focus on getting as much knowledge as you can out of the course, and your grade will be fine.

Religious Observances

If a you require flexibility on deadlines or modified exam dates as a result of religious observances, it is your responsibility to contact the course staff in the first two weeks of class (by Wednesday, September 18, 2024). Failure to do so may prevent accommodations from being made.

Academic Integrity

By virtue of enrollment, you agree to uphold the high academic standards of the University of Wisconsin–Madison; academic misconduct is behavior that negatively impacts the integrity of the institution. Cheating, fabrication, plagiarism, unauthorized collaboration, and helping others commit these previously listed acts are examples of misconduct which may result in disciplinary action. In this course, one example of misconduct would be copying or collaborating on an exam. Examples of disciplinary sanctions include, but are not limited to, failure on the assignment/course, written reprimand, disciplinary probation, suspension, or expulsion.

Accommodations for Students with Disabilities

The University of Wisconsin–Madison and this course support the right of all enrolled students to a full and equal educational opportunity. The Americans with Disabilities Act (ADA), Wisconsin State Statute (36.12), and UW–Madison policy (UW-855) require the university to provide reasonable accommodations to students with disabilities to access and participate in its academic programs and educational services. Faculty and students share responsibility in the accommodation process. You are expected to inform faculty (Ethan) of you need for instructional accommodations during the beginning of the semester, or as soon as possible after being approved for accommodations. I will work either directly with the you or in coordination with the McBurney Center to provide reasonable instructional and course-related accommodations. Disability information, including instructional accommodations as part of your educational record, is confidential and protected under FERPA. (See: McBurney Disability Resource Center)

Diversity & Inclusion

Diversity is a source of strength, creativity, and innovation for UW–Madison. The university and this course values the contributions of each person and respects the profound ways their identity, culture, background, experience, status, abilities, and opinion enrich the university and classroom community. We commit ourselves to the pursuit of excellence in teaching, research, outreach, and diversity as inextricably linked goals. The University of Wisconsin–Madison fulfills its public mission by creating a welcoming and inclusive community for people from every background—people who as students, faculty, and staff serve Wisconsin and the world.

Mental Health and Well-Being

Students, particularly graduate students, often experience stressors that can impact both their academic experience and personal well-being. These may include mental health concerns, substance misuse, sexual or relationship violence, family circumstances, campus climate, financial matters, among others.

Students are encouraged to learn about and utilize UW–Madison's mental health services and/or other resources as needed. Visit uhs.wisc.edu or call University Health Services at (608) 265-5600 to learn more.

You are also encouraged to alert the instructor (Ethan) if your mental or physical health or that of a loved one or family member is negatively impacting your ability to succeed in the course. We can then make appropriate accommodations.

Acknowledgements

This course (and some of the language in this syllabus) is adapted from Cornell University's Advanced Programming Languages course (CS 6110). The current version has evolved over many years, being taught by (at least): Andrew Myers, Dexter Kozen, Nate Foster, Adrian Sampson, and Alexandra Silva. Andrew Hirsch also helped with the construction and organization of the course. The language for the sections on academic integrity, disability accommodations, diversity & inclusion, and mental health is taken from standard UW–Madison syllabus resources.