- 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
- www Polymorphic typing of an algorithmic language - Xavier Leroy (PhD thesis)
- 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 - Programming Languages: Application and Interpretation - Shriram Krishnamurthi
- PAIP Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp - Peter Norvig, 1992
- 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
- Bird and Wadler - Introduction to Functional Programming, 1st Edition - Bird and Wadler
- AoP - The Algebra of Programming - Richard Bird, Oege de Moor
- www - Programming in Haskell - Graham Hutton, 2007
- RWH - Real World Haskell - Bryan O'Sullivan, Don Stewart, and John Goerzen
- 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
- www - Developing Applications With OCaml - Emmanuel Chailloux, Pascal Manoury and Bruno Pagano, 2000
- www - The Little Schemer - Daniel P. Friedman, Matthias Felleisen
- www - The Seasoned Schemer - Daniel P. Friedman, Matthias Felleisen
- www - The Little MLer - Matthias Felleisen, Daniel P. Friedman
- HTDP - How to Design Programs - Matthias Felleisen, Robert Findler, Matthew Flatt, Shriram Krishnamurthi
- 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