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.

Instructor

Jeremy Siek Luddy 3016 jsiek@indiana.edu

Lectures

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:

https://github.com/jsiek/B629-denotational/notes.pdf.

Office Hours

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

• or by appointment

Assignments

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.

• Homework 1 is due January 15
• Homework 2 is due January 22.
• Homework 3 is due January 29.
• Homework 4 is due February 14.
• Homework 5 is due February 28.
• Homework 6 is due March 26.
• Homework 7 is due April 11.
• Homework 8 is due TBD.

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

• Denotational semantics: a methodology for language development, Schmidt 1986.

• Outline of a Mathematical Theory of Computation, Scott 1970.

• The Denotational Semantics of Programming Languages, Tennent 1976.

• Simply Typed Lambda Calculus

  • Chapter 2 of Semantics of Programming Languages: Structures and Techniques. Gunter 1992.
  • A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. Chlipala 2007. Chaitanya Koparkar, April 16
  • Cartesian closed categories and typed λ-calculi. J. Lambek 1985. Jiawei Tang, February 28

• The Lambda Calculus: its Syntax and Semantics, Barendregt 1984.

• Lambda-Calculus And Combinators In The 20th Century. Cardone and Hindley, 2009. Yuquan Fu, April 23 (aka. History of Lambda-calculus and Combinatory Logic, 2006)

• Graph Models of the Lambda Calculus

  • Data Types as Lattices, Scott 1976.
  • Set-theoretical and other elementary models of the lambda-calculus, Plotkin 1993.
  • Algebras and combinators, Engeler 1981.
  • Revisiting Elementary Denotational Semantics, Siek 2017.

• Filter Models of the Lambda Calculus

  • Functional characterization of some semantic equalities inside lambda-calculus. Coppo, Dezani-Ciancaglini, Salle 1979.
  • A filter lambda model and the completeness of type assignment. Barendregt, Coppo, Dezani-Ciancaglini 1983.
  • Intersection Types and Lambda Models. Alessi, Barbanera, Dezani-Ciancaglini 2006.

• PCF

  • A type-theoretic alternative to ISWIM, CUCH, OWHY, Scott 1993.
  • LCF considered as a programming language, Plotkin 1977.

• The D∞ model of the λ-calculus

  • Lecture notes from Nate Foster's CS 6110 course

• Fixed point constructions in order-enriched categories. Wand 1979.

• The category-theoretic solution of recursive domain equations, Smyth and Plotkin, 1982.

• The Essence of Algol, Reynolds 1981.

• Notions of computation and monads, Moggi 1991.

• Full Abstraction

  • Observable sequentiality and full abstraction, Cartwright, Felleisen 1992. Ryan Scott, April 11
  • Full abstraction for the second order subset of an Algol-like language. Kurt Sieber, 1996.
  • Full Abstraction for PCF. Samson Abramsky, Radha Jagadeesan, Pasquale Malacaria 2000.