CSC2125H Fall 2023
Types and Programming Languages

Course Info

Instructor: Ningning Xie; email: ningningxie at cs.toronto.edu
Teaching Assistant: Tsung-Ju Chiang ; email: tsungju.chiang at mail.utoronto.ca
Lecture hours: 12-2 PM, Friday
Office hours:
  • Instructor: 3-4 PM, Friday, BA 3256
  • TA: 12-1pm, Tuesday, BA 3232
Quercus <----- New
Discussion: Ed
Contact Email: With subject "CSC2125H-F23: "

Course Overview

We will study programming languages viewed through the lens of their type structure. Half of the course will cover an introduction to programming language principles, and the other half will be reading group. After taking this course, students will be able to define programming languages via their type system and operational semantics, state and prove their properties, and appreciate the deep philosophical and mathematical underpinnings of programming language design.

Prerequisites:
The introductory part has no formal prerequisites, but an exposure of various forms of mathematical induction will be helpful.
Ideally, students should have already taken the following courses (or equivalent ones):
  • CSC324 Principles of Programming Languages
  • CSC2107/CSC488 Compilers and Interpreters
Grading & Evaluation:
  • Active learning: 10%
  • Three small-ish assignments: 15%
  • Paper presentation: 20%
  • Project (proposal 15%, presentation 20%, report 20%)

Relevant Textbooks

All textbooks below are supplementary, since our main source of reading materials will be lectures and research papers.

Course Schedule

The schedule below is tentative and subject to change throughout the semester.
Schedule Broad Area Notes Reading List
Week 1
Sept 15 		Course Overview & The Lambda Calculus [00-logistics] [01-lambda]
Homework 1 release [pdf] [source]
Week 2
Sept 22		 Recursion & STLC (just started) [02-recursion] [03-STLC-1]
Week 3
Sept 29 		STLC & From Lambda Calculus to Programming Languages [03-STLC] [04-eval]
(Ningning gone to Shonan; Tsung-Ju will give the lecture)
Homework 2 release (available on Quercus)
Week 4
Oct 6 		Parametric polymorphism & Products and sums [04.5-logistics] [05-poly] [06-sum]
Week 5
Oct 13 		Curry-Howard Correspondence & Calculus of constructions [07-prop] [08-coc]
(Note: we will take attendance this week)
Homework 3 release (available on Quercus)
Course project proposal due
Week 6
Oct 20 		Optional Q&A session
Week 7
Oct 27 		Paper reading: Gradual typing combines static and dynamic typing Background reading: Paper list:
Week 8
Nov 3 		Paper reading: Type lattice with intersections and unions Background reading: Paper list:
Reading week Nov 10 (No classes)
Week 9
Nov 17 		Paper reading: Language foundations beyond functional programming Try to grasp the high-level ideas:
  • Get a better understanding of the language
  • What are the main challenges in formalizing a language
  • What properties of the language do people get
Paper list:
Week 10
Nov 24 		Paper reading: Fancy types and where to find them Try to grasp the high-level ideas:
  • What are the types being discussed in the paper
  • What are they used for
  • What are the main techniques needed for them
Paper list:
Week 11
Dec 1 		Project presentation I
Week 12
Dec 8 		Project presentation II