diff -r 46f0dfedf9ef -r 7eaeae127955 src/Doc/manual.bib
--- a/src/Doc/manual.bib	Wed Jan 13 20:19:49 2016 +0100
+++ b/src/Doc/manual.bib	Wed Jan 13 21:15:23 2016 +0100
@@ -1012,6 +1012,17 @@
   note          = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
 }
 
+@inproceedings{Kuncar:2015,
+  author    = {Ondrej Kuncar},
+  title     = {Correctness of {Isabelle's} Cyclicity Checker: Implementability of Overloading
+               in Proof Assistants},
+  booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
+               {CPP} 2015, Mumbai, India, January 15-17, 2015},
+  year      = {2015},
+  url       = {http://doi.acm.org/10.1145/2676724.2693175},
+  doi       = {10.1145/2676724.2693175},
+}
+
 @inproceedings{Kuncar-Popescu:2015,
   author    = {Ondrej Kuncar and Andrei Popescu},
   title     = {A Consistent Foundation for {Isabelle/HOL}},