Programming Language Theory

Type Theory

Selected

1. How to prove it - Daniel J. Velleman
2. TaPL - Types and Programming Languages - Benjamin C. Pierce

Books

• SF - Software Foundations - Benjamin C. Pierce et al.
• PFPL - Practical Foundations for Programming Languages - Robert Harper
• ATTaPL - Advanced Topics in Types and Programming Languages - Edited by Benjamin C. Pierce (pdf)
• CPDT - Certified Programming with Dependent Types - Adam Chlipala
• SEwPR - Semantics Engineering with PLT Redex - Matthias Felleisen, Robby Findler, and Matthew Flatt. Redex
• HoTT - Homotopy Type Theory, Univalent Foundations of Mathematics
• Coq'Art Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions - Yves Bertot, Pierre Castéran.
• TTFP - Type Theory and Functional Programming - Simon Thompson, 1991
• PiMLTT - Programming in Martin-Löf's Type Theory, An Introduction - Bengt Nordström, Kent Petersson, Jan M. Smith
• PROT Proofs and Types - Jean-Yves Girard, Yves Lafont and Paul Taylor - 1987-90 pdf
• Using, Understanding, and Unravelling The OCaml Language — An introduction pdf
• Polymorphic typing of an algorithmic language (PhD Thesis) - Xavier Leroy pdf
• ATP - Handbook of Practical Logic and Automated Reasoning - John Harrison
• Basic Simple Type Theory - J. Roger Hindley pdf www paperback@booko
• Lambda Calculus and Combinators - J. Roger Hindley and Jonathan P. Seldin www pdf
• Semantics with Applications: An Appetizer - Hanne Riis Nielson, Flemming Nielson pdf
• An Introduction to Lambda Calculi for Computer Scientists - Chris Hankin
• The Definition of Standard ML (Revised) - Milner, Fofte, Harper, and MacQueen
• The Definition of Standard ML (1990) and Commentary on Standard ML (1991) www definition pdf commentary pdf

Papers

• Lambda Calculi with Types — Henk Barendregt pdf
• A Tutorial Implementation of a Dependently Typed Lambda Calculus - Andres Löh, Conor McBride and Wouter Swierstra www pdf, was previously published as "Simply Easy" pdf

Videos

• OPLSS
  • OPLSS 2014 - Oregon Programming Language Summer School 2014
  • OPLSS 2013 - Oregon Programming Language Summer School 2013
  • OPLSS 2012 - Oregon Programming Language Summer School 2012
  • OPLSS 2010 - Oregon Programming Language Summer School 2010
  • OPLSS 2011 - Oregon Programming Language Summer School 2011
• ICFP 2012 Monday keynote. Conor McBride: Agda-curious?

Programming Languages

Books

• CTM - Concepts, Techniques and Models of Computer Programming, Peter van Roby and Seif Haridi
• EOPL - Essentials of Programming Languages, 3rd Edition - Daniel P. Friedman
• PLAI-2nd - Programming Languages: Application and Interpretation - Shriram Krishnamurthi course with videos PLAI-1st
• PAIP Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp - Peter Norvig, 1992

Papers

• An argument against call/cc - Oleg Kiselyov www

Compiler Construction

Books

• LiSP - Lisp in Small Pieces - Christian Queinnec
• CwC Compiling with Continuations - Andrew W. Appel
• MCIiML Modern Compiler Implementation in ML - Andrew W. Appel
• pj-lester-book Implementing functional langauges: a tutorial - Simon Peyton Jones and David Lester, 1992
• slpj-book-1987 - The Implementationn of Functional Programming Languages - Simon Peyton Jones - 1987

Papers

• ZINC - The ZINC experiment, an economical implementation of the ML language - Xavier Leroy (Technical Report) more OCaml papers

Videos

• Coursera - Stanford - Compilers - Alex Aiken

Runtime systems

Books

• The Garbage Collection Handbook, The Art of Automatic Memory Management - 2011 - Richard Jones, Antony Hosking, Eliot Moss - www

Papers

• Lambda: The Ultimate GOTO - Debunking the 'Expensive Procedure Call' Myth, or, Procedure Call Implementations Considered Harmful, or, Lambda: The Ultimate GOTO - 1977 - Guy Lewis Steele, Jr. pdf

Functional Programming

Selected

1. Bird and Wadler - Introduction to Functional Programming, 1st Edition - Bird and Wadler

Books

• AoP - The Algebra of Programming - Richard Bird, Oege de Moor
• Programming in Haskell - Graham Hutton, 2007 www
• RWH - Real World Haskell - Bryan O'Sullivan, Don Stewart, and John Goerzen
• [FPiS] (http://www.manning.com/bjarnason/) - Functional Programming in Scala - Paul Chiusano and Rúnar Bjarnason
• SICP, Structure and Interpretation of Computer Programs, by Abelson, Sussman, and Sussman
• PCPH - Parallel and Concurrent Programming in Haskell - Simon Marlow
• RWOC - Real World OCaml - Jason Hickey, Anil Madhavapeddy, and Yaron Minsky
• Developing Applications With OCaml - Emmanuel Chailloux, Pascal Manoury and Bruno Pagano, 2000 www
• BTLS - The Little Schemer - Daniel P. Friedman, Matthias Felleisen
• BTSS - The Seasoned Schemer - Daniel P. Friedman, Matthias Felleisen
• BTML - The Little MLer - Matthias Felleisen, Daniel P. Friedman
• HTDP - How to Design Programs - Matthias Felleisen, Robert Findler, Matthew Flatt, Shriram Krishnamurthi
• HR - The Haskell Road to Logic, Maths and Programming - 2nd Ed. - Kees Doets, Jan van Eijck pdf
• A Book of Abstract Algebra - 2nd Ed. - Charles C. Pinter booko
• Lectures on the Curry-Howard Isomorphism pdf
• Purely Functional Data Structures - Chris Okasaki phd-thesis in pdf paperback@booko More purely functional data structures

Papers

• Lambda Papers - Lambda: The Ultimate Imperative/Declarative/GOTO - Guy Steele and Gerald Sussman
• Exploring Generic Haskell (PhD thesis) - Andres Löh. This an epic, assessible, book-length PhD on datatype generic programming.

Videos

• C9 Lectures: Dr. Erik Meijer - Functional Programming Fundamentals www
• C9 Lectures: Dr. Ralf Lämmel - Going Bananas + Advanced Functional Programming www
• Datatype-Generic Programming in Haskell - Andres Löh - slides in pdf

Category Theory

Selected

1. Conceptual Mathematics, A First Introduction to Categories, 2nd Edition - F. William Lawere and Stephen H. Schanuel
2. CTCS-2nd Category Theory for Computing Science - Michael Barr and Charles Wells CTCS-1st

Books

• Topoi, The Categorical Analysis of Logic, Robert Goldblatt pdf
• TTT - Toposes, Triples and Theories - Michael Barr and Charles Wells
• Category Theory Lectures Notes for ESSLLI - Michael Barr and Charles Wells pdf
• Category Theory for Scientists - David I. Spivak pdf
• Basic Category Theory for Computer Scientists - Benjamin C. Pierce

Other collections

• Great Works in Programming Languages - Collected by Benjamin Piece
• Classic Papers in Programming Languages and Logic - Karl Crary
• PLT Texts Online - Frank Atanassow
• Lambda the Ultimate - Ehud Lamm et al.
• Archives of Lambda the Ultimate (stale but includes "classic") - Chris Rathman
• Functional programming books overview — Alex (Alexey) Ott
• Programming Language People - Chris Rathman