Course lectures will be delivered virtually through Canvas, preferring Zoom which offers better performance and bandwidth in my experience, but using Collaborate Ultra as a fallback. All lectures will be recorded, so asynchronous participation is possible, although I strongly encourage students to attend synchronously to ask questions and engage with inclass activities.
You are encouraged but not required to use video chat. Video chat will help everyone engage and connect with each other and make for a more engaging course. However, we know that this may not be possible for all those attending the course.
You are also encouraged but not required to attend lectures synchronously. Lectures will be recorded and provided to you in some way (most likely through Canvas).
The course staff will hold regular synchronous office hours (schedule can be found under Resources), and you can email us to schedule meetings if these time slots do not work for you.
We will heavily use Piazza (see below) to facilitate additional asynchonous activities and discussion.
The course will rely on an honour code and not make use of invasive invigilation software.
Programming languages are a fundamental part of computer science. This course introduces the formal tools needed to describe precisely what a program means. These tools help us answer many useful questions about program analyses and transformations, such as:
Topics include:
This course is intended for graduate students in computer science. There are no formal course prerequisites, but you are expected to have the kind of mathematical maturity typical of one who has taken an undergraduate discrete math or theory of computation course. We will explicitly cover proof techniques in this course, so don't worry if you are rusty or not very familiar. Here are some resources I find helpful for refreshing or improving your skill at writing proofs:
To facilitate discussion among students in the class and
myself, we are using the Piazza Q&A platform. The system
allows you to ask questions, refine answers as a group, carry
on followup discussions, and disseminate relevant information.
Rather than emailing questions to me, I ask that you post your
questions to Piazza. If you have any problems or feedback for
the developers, email team@piazza.com.
Find our class
page
here
.
This course has no required textbook. Material will primarily be provided in a set of notes and/or covered in class, as well as through some supplementary readings. The material we cover will draw from a variety of sources.
The following books are recommended but not required:There will be an inclass midterm exam (date TBD).
Students will give a final presentation to the class on a topic of their own choosing related to Programming Language Principles.
There will be approximately 6 homework assignments during
the course of the semester. Homeworks will
I recommend that homeworks be typeset using the LaTeX
document preparation system, but will not require it:
you have the option to prepare your homework by hand, so long
as you make sure that it is clearly legible by me. I plan to
provide LaTeX templates for you, so this is a good chance to
learn one of the more common tools for writing academic
computer science papers, though the learning curve may be
steep at first. I'm happy to give guidance on how to work
with LaTeX (though I probably don't know all the latest tricks).
You can turn in assignments electronically as PDFs either
scanned or generated by LaTeX.
Assignments must be your individual work. You may discuss the homeworks with others, but you must write up and hand in your own solutions. In particular, follow the whiteboard policy: at the end of the discussion the "whiteboard" must be erased and you must not transcribe or take with you anything that has been written on the board (or elsewhere) during your discussion. You must be able to reproduce the results solely on your own after any such discussion.
Do not draw upon solutions to assignments (or in notes) from similar courses, nor use other such materials (e.g., programs) from any website or other external source in preparing your work.
The final grade will be comprised of the following components, with the following plan for distribution of marks (subject to revision):
The following resources are to help you succeed in the class.
The following is a draft course schedule, based on a prior offering of the course. The exact details (including some topics) will vary depending on the content covered in class and the interests and needs of the students (and myself).
I often update the notes as the term goes along. They are timestamped, so that you can tell when the most recent version was uploaded (note that the timestamp is distinct from the original date of creation).
Under Construction!#  Date  Topics  Notes  Supplementary Readings  

0  Wed, Sep 9  Course Introduction  
1  Mon, Sep 14  Modeling Programming Languages; Set Theory and Logic  Modeling Languages Set Theory Proof Techniques 

2  Wed, Sep 16  More on Set Theory and Logic  
3  Mon, Sep 21  B: A Language with many programs and few results Inductive Definitions Derivations as Data Structures 
Inductive Definitions Proof by Induction 
Proving Something False  
4  Wed, Sep 23  Principles of Induction Derivations cont'd. From Inversion to Parsing Parsing as Proof Search; Parsers as Theorem Provers 
Proof Techniques Proving Something False 

5  Mon, Sep 28  HW1 Review  
6  Wed, Sep 30  Operational Semantics

BS Notes Video on Operational Semantics 
SS Notes RS Notes AM Notes 

7  Mon, Oct 5  Postcards from 509 Backwards Reasoning Principles 

8  Wed, Oct 7  More Imp: From Inversion to Interpreters A Taste of Divergence Big Picture Review Formal propositional logic and Formal English 

9  Mon, Oct 12  Thanksgiving: No Class  
10  Wed, Oct 14  HW2 Highlights The Truth™ About Inductive Definitions and Induction Principles Coinductive Definition: A Counterpoint to Inductive Definition Modeling Divergence 
Coinduction Notes 

11  Mon, Oct 19  Proof by Coinduction  
12  Wed, Oct 21  Lexical Variables 1  SS Notes RS Notes AM Notes Lexical Binding Notes 

13  Mon, Oct 26 
Lexical Variables 2 Introduction to Procedures 
Lexical Binding Notes
Procedures Using Procedures 

14  Wed, Oct 28  StorePassing Semantics and Mutable References 
Mutable References  
15  Mon, Nov 2  Compilers: SemanticsPreserving CrossLanguage Translators Variable Scoping and Environments 
Environments  
16  Wed, Nov 4  Lexical Scoping vs. Dynamic Scoping Choose Your Own Induction Principle 
Environments and Scoping
Induction Unchained! 

17  Mon, Nov 9  Choose Your Own Induction Principle Exceptions 
Induction Unchained! Exceptions 

18  Wed, Nov 11  Rememberance Day: No Class  
19  Mon, Nov 16  Proper Tail Calls Abstracting Abstract Syntax (GĂ¶del Numbering) 
Tail Calls 

20  Wed, Nov 18  Type Systems  
21  Mon, Nov 23  Type Systems 2  
22  Wed, Nov 25  Braxton and Noa on Typescript and Gradual Typing Alison and James on Church Encoding (sans rapbattle) 

23  Mon, Nov 30  Katharine and Ramon on Finn, John, and Arsh on Formal Logic and Coq 

24  Wed, Dec 2  No class; Exam Assigned  