This course is a follow-on to 15-312 Foundations of Programming Languages concerned with a fuller development of the ideas broached therein.  The goal is to bring students up to speed on the basic tools of semantics of programming languages required to read contemporary literature.  Topics include:

• Advanced type systems, including call-by-push-value, algebraic effects, and dependent types.
• Equational theories of program behavior.
• Logical relations over an operational semantics defining semantic equality.
• Verification of the soundness of equational theories.
• Phase distinctions in programming languages as applied to cost analysis and program module systems.

This being the " release" of the course, the exact set of topics is to be determined.  Students are advised to expect "turbulence" in the delivery of the course!  The course does not, at present, satisfy any degree requirement.

The following resources are provided for students' reference:

• Practical Foundations of Programming Languages (Second Edition), Cambridge University Press, 2016.
• Piazza Discussion Group
• Zotero library of documents and references: https://www.zotero.org/groups/5339313/advanced_topics_in_pl_theory
• Readings provided in the Modules section of this course page.
• Lecture notes taken by students, also in the Modules section.

Participation for all students consists of these requirements:

• Preparation of one week's course notes in collaboration with another student, to be provided no later than one week after the lectures are given.  Please use the PFPL Syntax Macros for typesetting.
• Weekly homework assignments, which involve both written exercises and mechanizations using the Agda prover.  Homework assignments are released on Thursday at 6pm of each week, and are due by 6pm Wednesday of each week.
• Preparation of a final project jointly with another undergraduate student presenting a thorough account of some topic in PL's using the methods developed in this class.
• Commentary on the project report of at least two other students in the class, which will be posted on the Canvas page for easy reference.

Participation for graduate students consists of the foregoing requirements, plus

• Solving any advanced problems given in any homework.
• Preparation of a final project jointly with another undergraduate student presenting a thorough account of some topic in PL's using the methods developed in this class.  The development is to be at a more advanced and thorough level than required for undergraduates.
• Commentary on the project report of at least two other students in the class, which will be posted on the Canvas page for easy reference.

The teaching assistant for this class is Harrison Grodin, who will be responsible for setting and grading assignments.  He will also offer help with getting started with Agda for those students unfamiliar with this tool.

Undergraduates will be assigned a letter grade of A for full participation in the course with satisfactory grades on all homework.  Graduate students will be assigned Pass for their full participation as described above.  Students who fail to complete any requirements will not be assigned a passing grade.