CPSC 509: Programming Language Principles

Term 1 (Fall), 2018-2019
Mon. & Wed. 3:00pm - 4:30pm
DMP 201


Ronald Garcia
Office: ICICS 387
Office hours: To Be Determined


Course Description

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:

Familiarity with a functional programming language (e.g., Scheme, Racket, ML, Haskell) is useful but is not required. We will use the Racket programming language at times in the course to help reinforce the connection between the mathematics and programs/programming. I will introduce any needed programming concepts in class.


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 be 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: Some other useful texts that provide a different perspective or more depth in some areas are:


There will be an in-class midterm exam (date TBD).

Final Presentation

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 PDF's 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 web site or other external source in preparing your work.

Grading Policy

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.

Course Schedule

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
1 Sep 5 Course Introduction
2 10 Modeling Programming Languages;
Set Theory and Logic
Modeling Languages
Set Theory
3 12 B: A Language with many programs and few results
Inductive Definitions
Proof by Induction
Inductive Definitions
Proof by Induction
Proof Techniques
Proving Something False
4 17 First-Order Set Theory
Proof Techniques (Structure follows Proposition)
Proof Techniques
Proving Something False
5 19 HW1 Review
The Truth™ About Inductive Definitions and Induction Principles
6 24 Video on Operational Semantics: (Ron Out Of Town: ICFP)
  • Natural (Big-Step) Semantics
  • Structural Operational (Small-Step) Semantics (S.O.S.)
  • Reduction Semantics
  • Abstract Machines
BS Notes
SS Notes
RS Notes
AM Notes
7 26 Guest Lecturer (Ron Out Of Town: ICFP)
Syntax: Parsing as Proof Search
From Inversion Lemmas to Implementations
8 Oct 1 Proofs are Programs (Certifying Interpreters)
9 3 You Can't Even Define All The Functions (?!?)
Inter-Relating Operational Semantics Styles
8 Thanksgiving: No Class
10 10 HW2 Review?
Lexical Variables 1
11 15 HW3 Review
Review of Inversion Lemmas
Lexical Variables 2
Lecture 10 Notes
12 17 (Bound Variable) Names Are For Gravestones: α-equivalence classes Lecture 10 Notes
13 22 Procedures and Recursion Procedures
More Procedures
14 24 Choose Your Own Induction Principle
Variable Scoping and Environments
Induction Gone Wild!
15 29 Environment-Passing Semantics
Lexical Scoping vs. Dynamic Scoping
Store-Passing Semantics and Mutable References
Mutable References
16 31 Proper Tail Calls
Modeling Divergence
Tail Calls
17 Nov 5 Abstracting Abstract Syntax (Gödel Numbering)
18 7 Type Systems
19 12 Remembrance Day: No Class
20 14 Exam
16 19 Boyan: Automatic Differentiation
Chris: Action Semantics
17 21 Kumseok: Observational Equivalence in JavaScript
Nabil: Undefined Behaviour in C
Observational Equivalence
Undefined Behaviour
18 26 Adam and Wilder: Pi Calculus Slides
Go Examples
19 28 Nico and Renato: Session Types Slides

Last modified: Mon Dec 06:52:44 UTC 2018 by ronaldgarcia