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: | Tues/Thur 11:00 – 12:15pm |
Meeting Location: | Engineering Hall 3355 |
Instructor: | Ethan Cecchetti |
Instructor Contact: | cecchetti@wisc.edu |
Instructor Office: | Morgridge Hall 7649 |
Office Hours: | Tuesdays, 2:00 – 3:00pm or by appointment |
This schedule is tentative and subject to change.
Date | Topic | Notes | Assignment |
---|---|---|---|
Sept 4 | Welcome, Course Overview, & Preliminaries | [Syllabus] [Slides] |
Optional: Useful background material
OCaml Programming: Correct + Efficient + Beautiful
|
Core Topics | |||
Sept 9 | Inductive Definitions and Semantics | ||
Sept 11 | Structural and Well-Founded Induction | ||
Sept 16 | The IMP Language | ||
Sept 18 | Denotational Semantics | ||
Sept 23 | Axiomatic Semantics and Hoare Logic | ||
Sept 25 | Separation Logic | ||
Sept 30 | λ-calculus | ||
Oct 2 | λ-calculus Encodings | ||
Oct 7 | Reduction Strategies and Evaluation Contexts | ||
Oct 9 | Semantics by Translation | ||
Oct 14 | No Class (Ethan at OOPSLA) | ||
Oct 16 | No Class (Ethan at OOPSLA) | ||
Oct 21 | Recursive Functions | ||
Oct 23 | Functional Language | ||
(Oct 24) | Midterm Available | ||
Oct 28 | Continuations and Exceptions | ||
Oct 30 | State | ||
(Oct 31) | Midterm Due | ||
Nov 4 | Typed λ-calculus | ||
Nov 6 | Products, Sums, and Datatypes | ||
Nov 11 | Type Inference | ||
Nov 13 | Polymorphism and System F | ||
Nov 18 | Recursive Types | ||
Nov 20 | Subtyping | ||
Nov 25 | Logical Relations and Normalization | ||
Nov 27 | No Class (Thanksgiving) | ||
Special Topics | |||
Dec 2 | Information Flow Control and Noninterference | ||
Dec 4 | Abstract Interpretation | ||
Dec 9 | Wrap-up | ||
(Dec 11) | Final Available | ||
(Dec 16) | 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 Thursday, September 18, 2025). 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.