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)

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

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 Level Programming

• Faking it: Simulating Dependent types in Haskell

Dependent Type Theory

• Syntax and Semantics of Quantitative Type Thoery
  • Reason: Idris2, named Blowden type system is based on this paper.