Papers to Read

Jump to bottom

Jeffrey M. Young edited this page Mar 4, 2020 · 43 revisions

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

Links to external lists:

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?

Must Reads