Topics in Programming Languages: Denotational Semantics, Spring 2018 Course at Indiana University
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.
GunterCh2.pdf STLC Jan 19, 2018
Lambda2_1.pdf check Feb 7, 2018
Lambda5_3.pdf check Feb 7, 2018
Lambda5_4.pdf check Feb 7, 2018 check May 7, 2018
ScottDTL1976.pdf check Feb 22, 2018
all.bib check Dec 4, 2017
d-infinity.rkt finished solutions Mar 30, 2018 hw1 and hw2 Jan 8, 2018 added ex 7 Jan 16, 2018 typo Jan 23, 2018 ex 5.8.7 Feb 8, 2018 check Feb 22, 2018 check Mar 9, 2018 finished solutions Mar 30, 2018 finished solutions Mar 30, 2018
notes.tex check May 7, 2018
scribbles.txt hw 5 Feb 19, 2018
topology.tex merge Feb 19, 2018
tufte-common.def progress on denot of lambda Nov 5, 2017
tufte-handout.cls initial Nov 3, 2017

B629 Topics in PL: Denotational Semantics

Indiana University, Spring 2018

In this course we shall study the denotational semantics of programming languages, including the classic domain-theoretic models as well as elementary models based on functions-as-graphs and intersection types. The course assignments will include readings from selected chapters and papers, written homework, presentations, and some programming.


Jeremy Siek Luddy 3016


9:30-10:45am MW in Luddy Hall Room 3069 (not BH 305!), backup location Luddy Hall Room 4069.

The lecture notes are in progress at:

Office Hours

  • 11:00am-12 Thursdays in my office Luddy 3016,

  • or by appointment


There will be a homework (reading and some exercises) each week and a written report and presentations at the end of the semester. Also, roughly each week, one student will give a 30 minute presentation of a paper that the class has read.

Week-by-week Schedule

  1. Basics of denotational semantics
  2. Fixed point semantics
  3. Semantics of the simply-typed lambda calculus
  4. Semantics of the untyped lambda calculus
  5. Scott and Engeler's graph models
  6. Plotkin's graph model
  7. Filter models of the untyped lambda calculus
  8. More on filter models
  9. D-infinity model of the untyped lambda calculus
  10. Category-theoretic solutions to domain equations
  11. More on category-theoretic solutions to domain equations
  12. Semantics of PCF
  13. Full abstraction
  14. Semantics for imperative languages
  15. Monads and effect-handlers
  16. Student Presentations

Representative Readings