CPSC509: Programming Language Principles

When/Where

• Term 2 (Spring), 2023-2024
• Tues. & Thurs. 3:30pm - 5:00pm
• DMP 101

Instructor

• Name: Ronald Garcia
• Office: ICICS 387
• Email: rxg@cs.ubc.ca
• Office hours: Wednesdays, 1:30pm-3:00pm (online)

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:

• Is this program correct?
• Will this program encounter a run-time error?
• Is one program indistinguishable from another?
• Is this optimization a safe program transformation?
• Can programs written in this language crash?
• Is this compiler translation correct?
• Can source language A be translated into target language B?

Topics include:

• How to precisely specify the dynamic behavior of programs in some language;
• Methods for reasoning statically about the behavior of programs, particularly by specifying a type system for a language;
• Formally stating and proving properties of individual programs and entire programming languages;
• A formal treatment of important programming language features such as variables, functions, exceptions, mutable variables, type polymorphism, subtyping, and objects.

Prerequisites

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 study logical specification and 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:

• How to Prove it: A Structured Approach by Daniel J. Velleman
• How to Read and Do Proofs by Daniel Solow

Materials

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 as alternative sources of information about topics from this course:

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002. (E-BOOK)
• Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction. (E-BOOK)

Some other useful texts that provide a different perspective or more depth in some areas are:

• Robert Harper, Practical Foundations for Programming Languages, Cambridge University Press, 2012. (E-BOOK)
• Benjamin C. Pierce, ed., Advanced Topics in Types and Programming Languages, MIT Press, 2005. (E-BOOK)
• John C. Mitchell, Foundations for Programming Languages., MIT Press, 1996.
• Carl Gunter, Semantics of Programming Languages: Structures and Techniques , MIT Press, 1992.
• Matthias Felleisen et al., Semantics Engineering with PLT Redex , MIT Press, 2009.
  Part I of this book improves on a handy set of course notes on Programming Languages and Lambda Calculi.

Exams

There will be one comprehensive exam (date TBD).

Homeworks

There will be approximately 6 homework assignments during the course of the semester. 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 to Gradescope

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):

• Participation (15%). This includes asking and answering questions in class and on Piazza, volunteering to solve problems in class, and posting interesting course-related pointers to Piazza.
• Homework (50%). There will be approximately six homework assignments during the term. You have a week to complete each assignment and may work with your classmates (see above!).
• Comprehensive Exam (35%). This exam is at the end of the content portion of the course. The exam exercises your ability to analyze, create, and reason about language semantics and programs.

Resources

The following resources are to help you with your class work.

• LaTeX Resources Since you will be using LaTeX to typeset your homework, I provide some style files, as well as a cheat sheet to help you figure out how to typeset some things.
  1. Course-Specific Files:
     1. defs.tex: common definitions
     2. cpsc509-hw.sty: style file for homeworks.
  2. Latex Cheat Sheet (Source). Here are some examples of typesetting PL semantics, derivation trees, and whatnot.
  3. AMSMath Package Documentation. The American Mathematical Society provides some nice macros for typesetting. I use these a lot for typesetting languages.
  4. Semantic Package Documentation. This LaTeX Package has a number of features for typesetting mathematics. I prefer to use proof.sty (below) for derivations over the inference rules from here, since proof.sty produces more compact derivation trees.
  5. proof.sty Package (Documentation) These macros are nice for typesetting derivation trees.
  6. Leslie Lamport's Structure Proof LaTeX Package (COMING SOON!)
• Racket Resources We will be using the Racket dialect of Scheme to implement semantic artifacts in this class. Resources for learning and using Racket/Scheme will show up here soon!

Course Schedule (UNDER CONSTRUCTION!)

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).