Papers to Read

This page collects papers that we may want to read in future reading groups.

Links to external lists:

• Classic papers in PL and logic
• Great Works in PL (Curated by Benjamin Pierce)
• Papers we love: a bunch of great CS papers on a range of topics
• Classic Papers in PL and Logic (Curated by Karl Crary)

Conferences to check:

• ICFP
• PLDI
• POPL
• OOPLSA
• GPCE

Specific Papers mentioned in Reading Group

• Cardelli, Wegner, Understanding Types, Data Abstraction, and Polymorphism
  • This came up in reading group in reference to explaining modules with lambda calculus
• Linear Types can change the world!
  • Came up in reading group on Linearity Monad as a suggested introduction to the concept of linear types.
• A Phil Wadler paper on System F
  • Reason: Eric doesn't know System F (ed: lies!)

Let's see how well you really understand folds:

• Bananas and Lenses
  • Reason: This paper is a classic FP paper and lays the foundation for much of the lens library and Foldable, Traversable type classes in haskell
• Third Homomorphism Theorem
  • Reason: A pre-requisite for bananas-lenses this paper describes a theorem that allows you to know when you have a monoid. Again, very important for folds.
• Third Homomorphism Thoerem For Trees
  • Reason: This paper describes the third homomorphism theorem for trees and even relates that to Zippers! Speaking of which...

Monads

• Free/Freer monad (Oleg has a paper but we might need some simpler background first)
  • Reason: Understand the free monad design pattern for DSLs, get insight into the relationships between monads, monad transformers, effects, etc.

Old FP Papers:

• "Deforestation: Transforming programs to eliminate trees" by Philip Wadler

Type Level Programming

• Faking it: Simulating Dependent types in Haskell

Dependent Type Theory Papers

• Syntax and Semantics of Quantitative Type Thoery
  • Reason: Idris2, named Blowden type system is based on this paper.
• Truth of a Proposition, Evidence of a Judgment, Validity of a Proof
• An algorithm for type-checking dependent types
• Local Type Inference
• On Sense and Reference" (Über Sinn und Bedeutung)
• Constructive mathematics and computer programming
• Elimination with a motive
• Computation and Reasoning: A Type Theory for Computer Science This is a book

Generic Programming

• True Sums of Products

Type Theory Papers

• A Syntactic Approach to Type Soundness

Domain Specific Languages

• Reflect on Your Mistakes!

Category Theory

• Computation Types from a Logical Perspective

Other Papers

• "Differential Symbolic Execution" by Suzette Person, Matthew B. Dwyer, Sebastian G. Elbaum, and Corina S. Pasareanu
• Theorems For Free
• Theorems For Free For Free
• Zippers
  • Reason: Another classic, should be mandatory reading. This paper describes a functional structure known as a zipper that allows one to move up, down left or right in a tree elegantly and efficiently. Zippers also form the basic tree structure used in the programming language Clojure.
• The Marriage of Effects and Monads
  • Reason: This paper is the paper that relates Monads to Effects where they were previously separate lines of research.
• Hoare's hints on programming language design
  • Reason: Hoare's always a good read, and this paper details, comments on, and recommends solutions to many problems we still deal with today in PL design.
• Notation as a Tool of Thought
  • Reason: Seems interesting and is a Turing award speech, although rather long this could fit for a reprieve from more technically minded papers.
• Trouble Shared is Trouble Halved
  • Reason: A functional pearl that describes a tree with shared nodes called a nexus. This sounds a lot like a Tag tree with explicit sharing and without dimensions.
• Deriving Via
  • It's on GHC's new "deriving via" feature, which is a super elegant solution to making Haskell's type class deriving mechanism extensible, without requiring anything yucky like Template Haskell or generic programming.
• Type Safe Observable Sharing in Haskell
• Ghosts of Departed Proofs
• Incorrectness Logic
  • We typically design type systems around what is correct....but what if we designed around what is incorrect?
• RustBelt: Securing the Foundations of the Rust Programming Language
  • From POPL 2018. This paper was mentioned during topics discussion Spring 2020 (and Rust is interesting).
• A fully concurrent garbage collector for functional programs on multicore processors
• Generating compiler optimizations from proofs

Must Reads

• On the expressive power of programming languages
• Types as Abstract Interpretations
• Polymorphic Effect Systems

Selected Papers by Topic:

• Multiple Inheritance

  • Cardelli, Wegner: Understanding types, data abstractions, and polymorphism

  • Liskov: A Behavorial notion of subtyping

  • Cook, Hill and Canning: Inheritance is not subtyping

• Information Hiding

  • Parnas: criteria to be used in decomposing systems

  • Ostermann, Giarrusso, Kastner, Rendel: Revisiting information hiding

  • Findler and Flatt: Modular OOP with units and Mixins

• Lazy Evaluation

  • Ariola, Felleisen: The call-by-need lambda calculus

  • Wadsworth: Semantics and pragmatics of lambda-calculus

  • Peyton Jones: Implementation of Functional Programming languages

  • Peyton Jones: Spineless Tagless G-machine

• Objects

  • Cook: On understanding data abstraction, revisited

  • Cardelli, Wegner: Understanding types, data abstractions, and polymorphism

  • Liskov and Zilles: Programming with abstract data types

  • Nygaard and Dahl: The development of the Simula Languages

• Operator Overloading

  • Cardelli, Wegner: Understanding types, data abstractions, and polymorphism

  • Oliveira and Cook: Extensibility for the Masses

  • Synthesizing Object-Oriented and Functional Design to promote Re-use

  • Clifton et al: MultiJava: modular open classes and symmetric multiple dispatch for Java

• Generics

  • Oliveira and Cook: Extensibility for the Masses

  • Synthesizing Object-Oriented and Functional Design to promote Re-use

  • Wadler, Odersky, Stoutamire, Bracha: Adding Genericity to the Java Programming Language

• Reflection and Meta-Programming

  • Cantwell: Procedural reflection in programming languages

  • Demers and Malenfant: Reflection in logic, functional and object oriented programming: a Short comparative study

  • Mcllroy: Macro instruction extensions of compiler languages

  • The term homoicity comes from: Mooers et al: Programming languanges for non-numeric processing: TRAC, a text handling language

  • McCarthy: Recursive Functions of Symbolic Expressions and Their Computations by Machine, Part 1

  • Maes: Concepts and experiments in computational reflection

  • Chiba: Load-Time Structural Reflection in Java

• Type Inference

  • Damas and Milner: Principle type-schemes for functional programs

  • Milner: A thoery of type polymorphism in programming

  • Palsberg, Shwartzbach: Object-oriented type inference

  • Pottier: A Framework for Type inference with Subtyping

  • Type inference in Languages with subtyping (like most OOP) is problematic, see:

    • Pierce: Bounded quantification is undecidable

    • Curien, Ghelli: Coherence of subsumption

• Modules

  • Findler and Flatt: Modular OOP with units and Mixins

  • Parnas: criteria to be used in decomposing systems

  • (Book), Peirce: Advanced Topics in Programming Languages (See Chapter 8)

  • Ostermann, Giarrusso, Kastner, Rendel: Revisiting information hiding

  • Strnisa et al: The java module system: core design and semantic definition

• Substructural Type Systems and Memory Safety (linear types, affine types)

  • Garbage Collection

    • Invented in LISP: McCarthy: Recursive Functions of Symbolic Expressions and Their Computations by Machine, Part 1

    • Wilson: Uniprocessor garbage collection techniques

    • See also: Stefanovic et al: Older-first garbage collection in practice

    • and: Detlefs et al: Garbage-first garbage collection

  • Linear and Affine Types

    • Wadler: Linear types can change the world!

    • Tov, Pucella: Practical affine types

• Session Types (π calculus) and Concurrent programming

  • Dezani-ciancaglini and De'Liguro: Sessions and Session Types: An Overview

  • Gay et al: Modular session types for distributed OOP

  • Milner: The Polyadic pi-Calculus: A Tutorial

  • Dijkstra: Solution of a problem in concurrent programming control

  • Hewitt et al: A universal modular ACTOR formalism for artificial intelligence

• Lambdas and closures, in OOP languages

  • Fundamentals:

    • Anonymous functions: McCarthy: Recursive Functions of Symbolic Expressions and Their Computations by Machine, Part 1

    • Closures: Landin: The mechanical evaluation of expressions

  • Lambdas have been around since 1958 (LISP), Java got lambdas in 2014, Other papers of interest:

    • (Article) Bracha et al: Closures for the Java Programming Language

    • Cross the Gap from Imperative to Functional Programming through Refactoring

    • Khatchadourian: An Empirical Study on the Use and Misuse of Java 8 Streams

    • Khatchadourian: Safe automated refactoring for intelligent parallelization of Java 8 Streams

    • Mazinanian, Ketkar, Tsantalis, Dig: Understanding the use of lambda expressions in Java

More Compiler papers

• Dependently Typed Compilers don't go Wrong
• Calculating Correct Compilers
• Theorem proving for all: Equational Reasoning in Liquid Haskell
• Compiling a 50 year journey