- How to prove it - Daniel J. Velleman
- TaPL - Types and Programming Languages - Benjamin C. Pierce
- 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
- 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
- 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
- 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
- OPLSS 2010 - Oregon Programming Language Summer School 2010
- OPLSS 2011 - Oregon Programming Language Summer School 2011
- OPLSS 2012 - Oregon Programming Language Summer School 2012
- OPLSS 2013 - Oregon Programming Language Summer School 2013
- ICFP 2012 Monday keynote. Conor McBride: Agda-curious?
- 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
- An argument against call/cc - Oleg Kiselyov www
- 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
- ZINC - The ZINC experiment, an economical implementation of the ML language - Xavier Leroy (Technical Report) more OCaml papers
- Coursera - Stanford - Compilers - Alex Aiken
- The Garbage Collection Handbook, The Art of Automatic Memory Management - 2011 - Richard Jones, Antony Hosking, Eliot Moss - www
- 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
- Bird and Wadler - Introduction to Functional Programming, 1st Edition - Bird and Wadler
- 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
- 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.
- 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
- Conceptual Mathematics, A First Introduction to Categories, 2nd Edition - F. William Lawere and Stephen H. Schanuel
- CTCS-2nd Category Theory for Computing Science - Michael Barr and Charles Wells CTCS-1st
- 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
- 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
- Programming Language People - Chris Rathman