5/30 Data types as lattices
6/6 Continuous Lattices
6/13
6/20
6/27
7/4 Aaron away
7/11 Dan away
7/18 Dan away
7/25 Aaron away
8/1
8/8
8/15
8/22
8/29
9/5

Untyped λ-calculus, universal domains
The lattice of flow diagrams (1970) - Scott
Continuous Lattices (1972) - Scott
Data types as lattices (1976) - Scott
Domains for denotational semantics (1982) - Scott
What is a model of the lambda calculus? (1982) - Meyer
Models of the Lambda Calculus (1982) - Koymans
Gunter ch 8 (1992)

Domains and denotational semantics
Semantic Domains (1990, handbook) - Gunter, Scott
Denotational Semantics (1990, handbook) - Mosses
Domains for Denotational Semantics (1992) - Scott
Domains and Denotational Semantics: History, Accomplishments and Open Problems (1996) - Jung, et al.
SP82
Equilogical spaces, Scott et al

Monads, algebras, and effects
Monads and effects (2002) - Benton, Hughes, Moggi
Notions of computation and monads (1989) - Moggi
Computational lambda-calculus and monads (1989) - Moggi
An abstract view of programming languages (1990) - Moggi
Computational effects and operations: an overview (2002) - Plotkin, Power
Notions of computation determine monads (2002) - Plotkin, Power
The Category-Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads (2007) - Hyland, Power
Composing Monads using Coproducts (2002) - Lüth, Ghani
Combining computations effects: Commutativity and sum (2002) - Hyland, Plotkin, Power

Linear logic, *-autonomous categories, compact closed categories
A taste of linear logic (1993) - Wadler
  Alec's recommended introduction to linear logic
Categorical Semantics of Linear Logic For All (2006) - de Paiva
Linear logic, *-autonomous categories and cofree coalgebras (1985) - Seely

SOS
A structural approach to operational semantics - Plotkin
  I think Riccardo has a copy
SOS formats and meta-theory: 20 years after (2007) - Mousavi, Reniers, Groote

Mathematical operational semantics
Functorial Operational Semantics and its Denotational Dual (1996, phd) - Turi
Towards a Mathematical Operational Semantics (1997) - Turi, Plotkin
Category theory for operational semantics (2004) - Lenisa, Power, Watanabe
The expression lemma (2008) - Lämmel, Rypacek

Categorical programming
A Categorical Programming Language (1987) - Hagino
Categorical Programming with Inductive and Coinductive Types (2000, phd) - Vene
Charity (programming language)

Domain theory and topology
Vickers (chapter a week??)
Domain Theory in Logical Form (1991) - Abramsky
A Convenient Category of Domains (2007) - Battenfeld, Schöder, Simpson
Synthetic topology of data types and classical spaces (2004) - Escardó
Operational domain theory and topology of a sequential programming language (2005) - Escardó, Kin
Domains for computation in mathematics, physics and exact real arithmetic (1997) - Edalat
Continuous Lattices and Domains (2003) - Gierz, et al. (Supersedes "Compendium")

Applications of category theory
Some Aspects of Categories in Computer Science (1998) - PJ Scott
Physics, Topology, Logic and Computation: A Rosetta Stone (2008) - Baez, Stay
Topology and Category Theory in Computer Science (1991) - Reed, Roscoe, Wachter (eds.)

Polymorphism and parametricity
Theorems for free! (1990) - Wadler
Polymorphism is not set-theoretic (1984) - Reynolds

Full abstraction
Definability and Full Abstraction (2007) - Curien
Logical Full Abstraction and PCF (1997) - Longley, Plotkin

Game semantics
Semantics of interaction (1996) - Abramsky
Girard's Geometry of interaction? (Something about data types as vectors in a Hilbert space...)

Logical frameworks
A framework for defining logics (1987) - Harper, Honsell, Plotkin
The practice of logical frameworks (1996) - Pfenning

TIL/TAL, PCC
TIL: a type-directed optimizing compiler for Standard ML (1996) - Tarditi, et al.
From System F to typed assembly language (1999) - Morrisett, Walker, Crary, Glew
The design and implementation of a certifying compiler (1998) - Necula, Lee

Traced monoidal categories (recursion, feedback)
...

Topological representations of the λ-calculus (1999) - Awodey
Power domains and predicate transformers: A topological view (1983) - Smyth
Retracing some paths in process algebra (1996) - Abramsky
A very modal model of a modern, major, general type system (2007) - Appel et al.
Initial algebra semantics and continuous algebras (1977) - Goguen, Thatcher, Wagner, Wright
A syntactic approach to type soundness (1994) - Wright, Felleisen
On understanding types, data abstraction, and polymorphism (1985) - Cardelli, Wegner
The continuum as a final coalgebra (2002) - Pavlovic, Pratt
Chu spaces and their interpretation as concurrent objects (1995) - Pratt
Algebraic topology and concurrency (2006) - Fajstrup, Raußen, Goubault
Computing with Functionals: Computability Theory or Computer Science? (2006) - Normann
Call-by-name, call-by-value and the λ-calculus (1975) - Plotkin
Call-by-value is dual to call-by-name (2003) - Wadler
Foundations for structured programming with GADTs (2008) - Johann, Ghani
What is a Logic? (2000) - Mossakowski, Goguen, Diaconescu, Tarlecki
Macros that work (1990) - Clinger, Rees
Syntactic abstraction in Scheme (1993) - Dybvig, Hieb, Bruggeman
A type-theoretic interpretation of Standard ML (2000) - Harper, Stone
Abstract types have existential type (1988) - Mitchell, Plotkin
Abstracting control (1990) - Danvy, Filinski
A syntactic theory of sequential control (1987) - Felleisen, Friedman, Kohlbecker, Duba
Mobile ambients (1998) - Cardelli, Gordon
Functional programming with bananas, lenses, envelopes, and barbed wire (1991) - Meijer, Fokkinga, Paterson
On the expressive power of programming languages (1991) - Felleisen
The lambda calculus is algebraic (2002) - Selinger

Coalgebraic logic
Zippers, differentiating datatypes
Universal algebra (chapters from "Millenium edition" book)
TAPL, ATTAPL chapters
Recent papers from POPL, ICFP, ...

Categories (Awodey)
Yoneda
Adjoints
Monads

Categorical logic
Lambek & Scott
Goldblatt
Crole
Asperti & Longo
Awodey & Bauer (lecture notes)

Fall 2008
PPL
Decision Procedures
Logic reading group
Semantics, basic domain theory: Gunter, ch1–4

Spring 2008
Systems
Program analysis
Semantics: Gunter
  PCF: ch 4
  Finite approximation: ch 5
  Full abstraction: ch 6, Gordon
  Universal domains: ch 8, Scott, Meyer, ...

Summer 2008
Categories endgame
  Adjoint functor theorem
  Monads
  Kan extensions, (co)ends
Domain theory
  Pisa notes
  Mitchell
  SP82
  Domains in logical form - Abramsky
Game theory (and linear logic?)
Topology
  Vickers
Categorical logic, topoi, models for type theory
  Lambek & Scott
  Awodey, Bauer (lecture notes)
  Goldblatt
  Crole
  Asperti & Longo ?
  PER models, realizability, topoi
Coalgebra
  Modal/temporal logics
Concurrency (joint research-related reading?)
Misc.
  "Mathematical Structures for Semantics"
  Programming with comonads (cf. sigfpe)
  Differentiating types [McBride]

Fall 2008
Algorithms
Topology (course?), applications: topological domains, Stone duality, algebraic topology for concurrency
Parametricity, logical relations

Spring 2009
Computability, recursion theory, complexity, descriptive complexity (?)
Semantics
Lambda calculus: Hankin, Barendregt
Curry-Howard: Lecture Notes on CH, lambda cube / PTS
Type theory, CoC, Martin-Löf type theory

Summer 2009
Concurrency: process calculi, ...
Type systems: "syntactic" type theory, e.g. ATTaPL, polytypism

What is the story of PL and its theory? What have been the major research trends? The major breakthroughs? The major contributions to other areas of computing and the mathematical sciences? What are our guiding visions, major milestones, biggest embarrassments? Where is the field going and where has it been?

Readings from Matthias's HoPL course
Challenges for Theoretical Computer Science – some juicy bits on PL theory at the bottom

λ-calculus

Lambda Calculi – Hankin
Barendregt ...

Combinatory logic
Recursion theory

Domain theory

Gunter, ch 10
Pisa notes – Plotkin

Domain Theory in Logical Form – Abramsky

Category theory

Category Theory – Awodey

n-Cats: Higher Categories, Higher Operads

Categorical logic / Topoi

Topoi – Goldblatt
Introduction to Higher-Order Categorical Logic – Lambek, Scott

Sheaves in Geometry and Logic – Mac Lane, Moerdijk

Topology – Munkres

Dualities: equivalences between algebraic and topological structure
Algebraic topology for concurrency / distributed computing [...]

Universal algebra

Various free pdf's
Mitchell, ch 3
Lawvere's thesis

Synthetic topology - Escardó

Separation logic

Computational theory

(Concurrent with CSG7xx)

Theory of Recursive Functions and Effective Computability -- Rogers
Introduction to the Theory of Computation – Sipser
Theory of Computation – Kozen
Computability: A Mathematical Sketchbook – Bridges

Descriptive complexity

Semantics of Programming Languages – Gunter
Foundations for Programming Languages – Mitchell
The Formal Semantics of Programming Languages – Winskell

Alternative models

games (full abstraction for PCF)
realizability (?)
geometric ("cuboidal")

[Where did I find these referenced? -dan] 

Semantics, categorically

Functorial Operational Semantics and its Denotational Dual – Turi
Towards a mathematical operational semantics – Turi, Plotkin
Category theory for operational semantics – Lenisa, Power, Watanabe

Fixed points, categorically

Logical relations

Mitchell, ch 8-ish
ATaPL, ch ?

Types and Programming Languages – Pierce
Advanced Types and Programming Languages – Pierce

Categories, Types, and Structures – Asperti, Longo
Categories for Types – Crole

Curry-Howard

Proofs and Types – Girard, Lafont, Taylor
Lectures on the Curry-Howard Isomorphism – Sørensen and Urzyczyn
The Girard-Reynolds Isomorphism – Wadler

Pure type systems, λ-cube

e.g. calculus of constructions

Parametricity

(cf. logical relations)

Polytypism

Programming with types - Weirich
...

Macros

Module systems and their type theory (Dreyer thesis, chapter in ATTaPL)

Categorical abstract machine

Moggi's monads

Coalgebra, coinduction, corecursion

Non-well-founded Sets - Aczel
Vicious Circles – Barwise, Moss

Program construction

Categorical programming

A Categorical Programming Language – Hagino
Categorical Programming with Functorial Strength – Spencer
Categorical Programming with Inductive and Coinductive Types – Vene

Concurrency

A History of Process Algebra – good intro?

Theorem proving

(cf. Curry-Howard, calculus of constructions)

...

Security

Algorithmic information theory
...