/plt-study

A path to Programming Language Theory enlightenment

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
  • 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

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

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

Videos

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