Papers To Read

A list of papers I want to read, hopefully, the list doesn't just grow over time :D (Bolded ones have been read!)

Books:

• Type Systems, Luca Cardelli
• Category Theory for Programmers, Bartosz Milewski
• Homotopy type theory
• Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, Adam Chlipala
• Computation and Reasoning: A Type Theory for Computer Science, Zhaohui Luo
• The implementation of functional programming languages, Simon Peyton Jones
• Structure and Interpretation of Computer Programs, Harold Abelson and Gerald Jay Sussman with Julie Sussman
• Gödel, Escher, Bach by Douglas Hofstadter
• Category Theory for Programmers

From here and there:

• Type classes: an exploration of the design space, Simon Peyton Jones, Mark Jones, and Erik Meijer
• Why Functional Programming Matters, John Hughes
• An Axiomatic Basis for Computer Programming, C. A. R. Hoare
• An Introduction to Operational Semantics and Abstract Machines, Hayo Thielecke
• Programming with Astract Data Types, Barbara Liskov
• Functional Pearls: Monadic Parsing in Haskell, Graham Hutton and Erik Meijer
• The Next 700 Programming Languages, P. J. Landin
• Notions of Computation and Monads, Eugenio Moggi
• Monads for Functional Programming, Philip Wadler
• Section 4 of Local Type Inference, Pierce and Turner
• Contextual Modal Type Theory, ALEKSANDAR NANEVSKI, FRANK PFENNING, and BRIGITTE PIENTKA
• Gradual Typing for Functional Languages, Jeremy G. Siek and Walid Taha
• Refined Criteria for Gradual Typing, Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, andJohn Tang Boyland
• A Syntactic Approach to Type Soundness, Andrew K. Wright and Matthias Felleisen
• Algebra of Programming, Richard Bird and Oege de Moor
• Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, E. Meijer, M. Fokkinga, and R. Paterson
• Faking It: Simulating Dependent Types in Haskell, Conor McBride
• Deriving Via or, How to Turn Hand-Written Instances into an Anti-Pattern, Baldur Blöndal, Andres Löh, and Ryan Scott
• Gradual Refinement Types, Nico Lehmann and Éric Tanter
• Safe Zero-cost Coercions for Haskell, Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich
• True Sums of Products, Edsko de Vries and Andres Löh
• Making implicit parameters explicit, Atze Dijkstra and S. Doaitse Swierstra
• The Essence of the Iterator Pattern, Jeremy Gibbons and Bruno c. d. s. Oliveira.
• A Generic Deriving Mechanism for Haskell, José Pedro Magalhães, Atze Dijkstra, Johan Jeuring, and Andres Löh
• Giving Haskell a Promotion, Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães
• Computational types from a logical perspective, Benton, P.H., Bierman, G.M., and de Paiva, V.
• What the Tortoise said to Achilles, Carroll, L.
• Origins of recursive function theory, Kleene, S.
• Reflections of my advisor: stories of mathematics and mathematicians, Shell-Gellasch, A.E.
• Propositions as Sessions, Philip Wadler.
• FERRY — Database–Supported Program Execution, Torsten Grust, Manuel Mayr, Jan Rittinger, and Tom Schreiber.
• Avalanche-Safe LINQ Compilation,Torsten Grust, Jan Rittinger, and Tom Schreiber.
• Kleisli, a functional query system, Limsoon Wong.
• Domain Specific Embedded Compilers, Daan Leijen and Erik Meijer.
• On understanding types, data abstraction, and polymorphism, L. Cardelli and P. Wegner.
• Abstract types have existential type, J. C. Mitchell and G. D. Plotkin.
• Three approaches to type structure, J. C. Reynolds.
• Syntax and Semantics of Quantitative Type Theory, Robert Atkey.
• Dependent Type Providers, David Raymond Christiansen. --> add summary!
• Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection, David Raymond Christiansen.
• Elaborator Reflection: Extending Idris in Idris, David Christiansen and Edwin Brady.
• Banana Algebra: Compositional Syntactic Language Extension, Jacob Andersena, Claus Brabrandb, and David Raymond Christiansenb.
• Reflect on Your Mistakes! Lightweight Domain-Specific Error Messages, David Raymond Christiansen.
• Truth of a Proposition, Evidence of a Judgment, Validity of a Proof, Per Martin-Löf
• Total Functional Programming, D. A. Turner
• Type Inference, Haskell and Dependent Types, Adam Gundry --> looks like an interesting thesis

Refs from the Software Foundation series:

• A Gentle Introduction to Type Classes and Relations in Coq, Pierre Castéran

Refs from the Haskell Programming book:

• A Tutorial to Lambda Calculus, Ra´ul Rojas
• Introduction to Lambda Calculus, Henk Barendregt and Erik Barendsen
• Proofs and Types, JEAN-YVES GIRARD
• How to Make Ad-hoc Polymorphism Less Ad-hoc, Philip Wadler and Stephen Bolt
• The Expression Problem, Philip Wadler
• The Implementation of Functional Programming Languages, Simon Peyton Jones
• Fundamental Concepts in Programming Languages, Christopher Strachey (note: page 11: currying)
• Point-free Program Calculation, Manuel Alcino Pereira da Cunha
• A tutorial on the universality and expressiveness of fold, Graham Hutton
• Intro to FP using Haskell(1998), Richard Bird and Philip Wadler
• Type classes: an Exploration of the Design Space, Simon Peyton Jones, Mark Jones, and Erik Meijer
• A system of constructor classes: overloading and implicit higher-order polymorphism, Mark Jones
• Applicative Programming with Effects, C. McBride and R. Paterson
• Essence of the Iterator Pattern, J. Gibbons and B. Oliveira
• Constructing Applicative Functors, R. Paterson
• Idioms are oblivious, arrows are meticulous, monads are promiscuous, S. Lindley, P. Wadler, and J. Yallop
• Notation as a Tool of Thought, Kenneth E. Iverson

Languages/tools to play around with:

• Elm

Useful references:

• Practical Foundations for Programming Languages, Robert Harper

Books to read just for fun:

• Proofs from the Book, Martin Aigner and Gunter Ziegler
• On Numbers and Games, John Conway
• Haskell 98 Language and Libraries The Revised Report, S. P. Jones