--- a/LMCS-Paper/document/root.bib	Wed Feb 22 12:10:17 2012 +0000
+++ b/LMCS-Paper/document/root.bib	Wed Feb 29 03:12:52 2012 +0000
@@ -1,3 +1,12 @@
+
+@Unpublished{Traytel12,
+  author =       {D.~Traytel and A.~Popescu and J.~C.~Blanchette},
+  title =        {{F}oundational, {C}ompositional ({C}o)datatypes for {H}igher-{O}rder 
+                  {L}ogic: {C}ategory {T}heory {A}pplied to {T}heorem {P}roving},
+  note =         {Submitted for publication.},
+  year =         {2012}
+}
+
 @inproceedings{pfenningsystem,
   author =       "F.~Pfenning and C.~Sch{\"u}rmann", 
   title =        "{S}ystem {D}escription: {T}welf - {A} {M}eta-{L}ogical