Course Webpage for B522 Programming Language Foundations, Spring 2020, Indiana University

View the Project on GitHub jsiek/B522-PL-Foundations

B522 Programming Language Foundations

Indiana University, Spring 2020

In this course we study the mathematical foundations of programming languages. That is, how to define programming languages and how to reason about those languages and programs written in them. The course will use the online textbook

Programming Language Foundations in Agda (the beta version)

Agda is a proof assistant and a dependently typed language. No prior knowledge of Agda is assumed; it will be taught from scratch. Prior knowledge of another proof assistant or dependently typed language is helpful but not necessary.


Prof. Jeremy Siek, Luddy 3016, jsiek@indiana.edu


Monday and Wednesday at 4:30-5:45pm in Luddy Hall Room 4101.

Office Hours (in Luddy Hall 3016 or the neighboring 3014)



Month Day Topic
January 13 Naturals & Induction
  15 Relations
  16 Equality & Isomorphism (unusual day, regular time)
  27 Connectives & Negation
  28 Quantifiers & Decidable (unusual day, regular time)
  29 Lists and higher-order functions
February 3 Lambda the Simply Typed Lambda Calculus
  5 Properties such as type safety
  10 DeBruijn representation of variables
  12 More constructs: numbers, let, products (pairs), sums, unit, empty, lists
  17 Inference bidirectional type inference
  19 Untyped Lambda Calculus
  24 Confluence of the Lambda Calculus
  26 BigStep Call-by-name Evaluation of the Lambda Calculus
March 2 Denotational semantics of the Lambda Calculus
  4 Compositional
  9 Soundness
  11 Adequacy
  16 ContextualEquivalence
  18 References and the Heap
  23 Subtyping and Records
  25 Classes and Objects (Featherweight Java)
  30 Gradual Typing
April 1 Universal and Existential Types (Parametric Polymorphism)
  6 Hindley-Milner Inference
  8 Recursive Types
  13 Intersection and Union Types
  15 Higher-Order Polymorphism
  20 Dependent Types
  22 TBD
  27 TBD
  29 TBD