Index: doc/bibliography/pl.bib
===================================================================
--- doc/bibliography/pl.bib	(revision 71a12390eb03a6fdd2beefb60f5a0838f37b2ea8)
+++ doc/bibliography/pl.bib	(revision 39de1c5509618f7fa261127870a0d93070f254fa)
@@ -1148,4 +1148,11 @@
     year	= 1998,
     note	= {{\small\textsf{ftp://\-plg.uwaterloo.ca/\-pub/\-Cforall/\-refrat.ps.gz}}},
+}
+
+@phdthesis{Norrish98,
+  title={C formalised in HOL},
+  author={Norrish, Michael},
+  year={1998},
+  school={University of Cambridge}
 }
 
@@ -3154,4 +3161,25 @@
     year	= 2018,
 }
+
+@article{Leroy09,
+ keywords = {C formalization},
+ contributer = {a3moss@uwaterloo.ca},
+ author = {Leroy, Xavier},
+ title = {Formal Verification of a Realistic Compiler},
+ journal = {Commun. ACM},
+ issue_date = {July 2009},
+ volume = {52},
+ number = {7},
+ month = jul,
+ year = {2009},
+ issn = {0001-0782},
+ pages = {107--115},
+ numpages = {9},
+ url = {http://doi.acm.org/10.1145/1538788.1538814},
+ doi = {10.1145/1538788.1538814},
+ acmid = {1538814},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+} 
 
 @manual{Fortran95,
@@ -5316,4 +5344,23 @@
 }
 
+@inproceedings{Krebbers14,
+ keywords = {c formalization},
+ contributer = {a3moss@uwaterloo.ca},
+ author = {Krebbers, Robbert},
+ title = {An Operational and Axiomatic Semantics for Non-determinism and Sequence Points in C},
+ booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '14},
+ year = {2014},
+ isbn = {978-1-4503-2544-8},
+ location = {San Diego, California, USA},
+ pages = {101--112},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/2535838.2535878},
+ doi = {10.1145/2535838.2535878},
+ acmid = {2535878},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+} 
+
 @book{Deitel04,
     keywords	= {concurrency, operating systems},
@@ -7612,4 +7659,11 @@
 }
 
+@techreport{Black90,
+  title={Typechecking polymorphism in {Emerald}},
+  author={Black, Andrew P and Hutchinson, Norman C},
+  year={1990},
+  institution={Cambridge Research Laboratory, Digital Equipment Corporation}
+}
+
 @article{Cormack90,
     keywords	= {polymorphism},