diff --git a/README.md b/README.md
index 8aeaa6b..9bd6175 100644
--- a/README.md
+++ b/README.md
@@ -26,7 +26,7 @@ read closely on a second pass.
     but I think PFPL does a better job explaining the foundations it
     works from and then covers more topics I find interesting.
 
-    * [Online copy](http://www.cs.cmu.edu/~rwh/plbook/1sted-revised.pdf)
+    * [Online copy](http://www.cs.cmu.edu/~rwh/plbook/2nded.pdf)
     * [Dead-tree copy](http://www.amazon.com/Practical-Foundations-Programming-Languages-Professor/dp/1107029570/ref=sr_1_1?ie=UTF8&qid=1439346858&sr=8-1&keywords=practical+foundations+for+programming+languages)
 
  - Types and Programming Languages (TAPL)
@@ -51,6 +51,14 @@ read closely on a second pass.
 
    * [Online supplements](http://www.cis.upenn.edu/~bcpierce/attapl/)
    * [Dead-tree copy](http://www.amazon.com/exec/obidos/ASIN/0262162288/benjamcpierce)
+   
+ - Type Theory and Functional Programming (TTFP)
+   
+   * [Online Copy](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf)
+ 
+ - Practical Foundations of Mathematics (PFM)
+   
+   * [Online Copy](http://www.paultaylor.eu/~pt/prafm/html/)
 
 ### Proof Assistants
 
@@ -162,6 +170,7 @@ major proof assistants are
    * [Equality in Lazy Computation System](http://www.nuprl.org/documents/Howe/EqualityinLazy.html) (of general interest)
    * [Naive Computational Type Theory](http://www.nuprl.org/documents/Constable/naive.pdf)
    * [Innovations in CTT using NuPRL](http://www.nuprl.org/documents/Allen/05-jal-final.pdf)
+   * [Two Lectures on Constructive Type Theory](https://www.cs.uoregon.edu/research/summerschool/summer15/notes/OPLSS-Short-2015-2.pdf)
 
  - Homotopy Type Theory