Programming Language Theory (Temporary Page)

Mort Yao

[Wikipedia: Programming language theory]

1 Functional Programming

[Wikipedia: Functional programming]

Books:

  • How to Design Programs (HtDP) (by Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi) [Homepage] [HTML] [HTML (2nd Ed.)]
  • Structure and Interpretation of Computer Programs (SICP, “Wizard Book”) (by Gerald Jay Sussman, Hal Abelson, Julie Sussman) [Homepage] [HTML] [PDF (Unofficial)]
  • Introduction to Functional Programming (by Richard Bird, Philip Wadler) [PDF]
  • Pearls of Functional Algorithm Design (by Richard Bird)
  • Purely Functional Data Structures (by Chris Okasaki) [PDF]
    • StackExchange: What’s new in purely functional data structures since Okasaki? [Link]

2 Programming Paradigms

[Wikipedia: Programming paradigm]

Books:

  • Concepts, Techniques, and Models of Computer Programming (CTM, “Oz Book”) (by Peter Van Roy, Seif Haridi) [Homepage]

3 Programming Languages

Books:

  • Essentials of Programming Languages (EOPL) (by Daniel P. Friedman, Mitchell Wand, Christopher T. Haynes) [Homepage] [Code]
  • Programming Languages: Application and Interpretation (PLAI) (by Shriram Krishnamurthi) [Homepage] [HTML] [PDF]

4 Abstract Algebra

[Wikipedia: Abstract algebra]

Online resources:

  • Wikibooks: Abstract Algebra [HTML]

Books:

  • A Book of Abstract Algebra (by Charles C. Pinter)

4.1 Category Theory

[Wikipedia: Category theory]

Books:

  • Category Theory for Computing Science (CTCS) (by Michael Barr, Charles Wells) [Homepage] [PDF]
  • Basic Category Theory for Computer Scientists (by Benjamin C. Pierce)
  • Category Theory for Scientists (by David Spivak) [PDF] [Course Homepage (MIT 18-S996)]
  • Conceptual Mathematics: A First Introduction to Categories (by F. William Lawere, Stephen H. Schanuel)
  • Categories for the Working Mathematician (by Saunders Mac Lane)

5 Mathematical Logic and Foundations of Mathematics

[Wikipedia: Mathematical logic] [Wikipedia: Foundations of mathematics]

Online resources:

  • Wikibooks: Logic for Computer Scientists [HTML]

Books:

  • The Haskell Road to Logic, Maths and Programming (HR) (by Kees Doets, Jan van Eijck) [Homepage]
  • Introduction to Logic and to the Methodology of Deductive Sciences (by Alfred Tarski)
  • Mathematical Logic (by Stephen Cole Kleene)
  • Introduction to Metamathematics (by Stephen Cole Kleene)
  • The Foundations of Mathematics (by Kenneth Kunen)

6 Lambda Calculus

[Wikipedia: Lambda calculus]

Books:

  • An Introduction to Functional Programming Through Lambda Calculus (by Greg Michaelson) [PDF]
  • An Introduction to Lambda Calculi for Computer Scientists (by Chris Hankin)
  • Introduction to Lambda Calculus (by Henk Barendregt, Erik Barendsen) [PDF]
  • The Lambda Calculus, Its Syntax and Semantics (by Henk Barendregt)
  • Lambda Calculus with Types (by Henk Barendregt, Wil Dekkers, Richard Statman)

7 Type Theory

[Wikipedia: Type theory]

Online resources:

  • Software Foundations (SF) (by Benjamin C. Pierce, etc.) [HTML]

Books:

  • Types and Programming Languages (TAPL) (by Benjamin C. Pierce) [Homepage]
  • Advanced Topics in Types and Programming Languages (ATTAPL) (by Benjamin C. Pierce) [Homepage]
  • Practical Foundations for Programming Languages (PFPL) (by Robert Harper) [PDF (Online Preview)] [PDF (Working Draft)] [Course Homepage (CMU 15-814)] [Course Videos (CMU 15-819)]

  • Type Theory and Functional Programming (TTFP) (by Simon Thompson) [Homepage] [PDF]

  • Proofs and Types (ProT) (by Jean-Yves Girard, Yves Lafont, Paul Taylor) [Homepage] [PDF]
  • Implementing Mathematics with The Nuprl Proof Development System (“NuPRL Book”) (by Robert L. Constable, etc.) [Homepage] [HTML] [PS]
  • Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Coq’Art) (by Yves Bertot, Pierre Castéran) [Homepage]
  • Certified Programming with Dependent Types (CPDT) (by Adam Chlipala) [Homepage]

  • Homotopy Type Theory (HoTT) (by Univalent Foundations of Mathematics) [Homepage] [GitHub]

8 Compiler Construction

[Wikipedia: Compiler construction]

Books:

  • Language Implementation Patterns: Create Your Own Domain-Specific and General Programming Languages (by Terence Parr)
  • Lisp in Small Pieces (L.i.S.P) (by Christian Queinnec) [Homepage]
  • The Implementation of Functional Programming Languages (by Simon Peyton Jones) [Homepage] [PDF]
  • Implementing Functional Languages: A Tutorial (by Simon Peyton Jones, David Lester) [Homepage] [PDF]
  • Programming Language Pragmatics (by Michael L. Scott) [Homepage]
  • Compilers: Principles, Techniques, and Tools (“Dragon Book”) (by Alfred V. Aho, Monica S. Lam, Ravi Sethi, Jeffrey D. Ullman) [Homepage]
  • Engineering a Compiler (by Keith Cooper, Linda Torczon)
  • Modern Compiler Implementation in ML (MCIiML, “Tiger Book”) (by Andrew W. Appel) [Homepage]
  • Compiling with Continuations (CwC) (by Andrew W. Appel)
  • Program Logics for Certified Compilers (PLCC) (by Andrew W. Appel)

Complementary Lists