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 jsiek@indiana.edu
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.
-
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.
- 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.
- Basics of denotational semantics
- Fixed point semantics
- Semantics of the simply-typed lambda calculus
- Semantics of the untyped lambda calculus
- Scott and Engeler's graph models
- Plotkin's graph model
- Filter models of the untyped lambda calculus
- More on filter models
- D-infinity model of the untyped lambda calculus
- Category-theoretic solutions to domain equations
- More on category-theoretic solutions to domain equations
- Semantics of PCF
- Full abstraction
- Semantics for imperative languages
- Monads and effect-handlers
- Student Presentations
-
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.