This course provides a rigorous introduction to the principles of advanced programming languages and programming-languages theory. It covers important fundamentals used across different subfields of programming languages research and is designed to prepare you to understand and conduct research in programming languages.
The course is primarily a lecture course, with written homeworks and take-home exams throughout the semester. While motivated by practical applications, much of the content of this course will be theoretical. Some familiarity with functional programming, formal logic, or basic programming languages theory is strongly encouraged. Those lacking this background may wish to take a course such as COMP SCI 538 or work through online materials such as Michael Clarkson's "OCaml Programming: Correct + Efficient + Beautiful."
This course does not have an official or required textbook. If you want separate reference documents, the following two texts are excellent in combination:
For a detailed list of topics, please see the course schedule tab. For more details on goals an expectations, please see the syllabus.
Meeting Time: | Mon/Wed/Fri 11:00 – 11:50am |
Meeting Location: | Computer Sciences 1325 |
Instructor: | Ethan Cecchetti |
Instructor Contact: | cecchetti@wisc.edu |
Instructor Office: | CS 7395 |
Office Hours: | Wednesdays, 2:00 – 3:00pm or by appointment |
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
|
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 |
(A pdf version of this syllabus is available here.)
By the end of the course, you will be able to:
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.
The assignments in this course will consist of problem sets and exams, all handed in on Canvas.
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 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.
Grades will be based on the following breakdown:
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 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 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 grades will be based on two components:
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.
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.
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.
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 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.
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.
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.