LMCS-Paper/document/root.bib
changeset 3160 603a36f19bfe
parent 3130 8fc6b801985b
--- a/LMCS-Paper/document/root.bib	Thu Apr 12 01:39:54 2012 +0100
+++ b/LMCS-Paper/document/root.bib	Thu Apr 19 15:39:46 2012 +0100
@@ -3,7 +3,7 @@
   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},
+  note =         {To appear in \emph{Proc.~of the 27th Symposium on Logic in Computer Science (LICS)}},
   year =         {2012}
 }
 
@@ -112,12 +112,14 @@
   pages =        {173--184}
 }
 
+
 @Unpublished{chargueraud09,
-  author       = "A.~Chargu{\'e}raud",
-  title        = "{T}he {L}ocally {N}ameless {R}epresentation",
-  Note         = "To appear in Journal of Automated Reasoning."                  
+   author = "A.~Chargu{\'e}raud",
+   title = "{T}he {L}ocally {N}ameless {R}epresentation",
+   note = "To appear in \emph{Journal of Automated Reasoning}"
 }
 
+
 @article{NaraschewskiNipkow99,
   author={W.~Naraschewski and T.~Nipkow},
   title={{T}ype {I}nference {V}erified: {A}lgorithm {W} in {Isabelle/HOL}},
@@ -155,7 +157,7 @@
 }
 
 @Unpublished{Pitts04,
-  author = 	 {A.~Pitts},
+  author = 	 {A.~M.~Pitts},
   title = 	 {{N}otes on the {R}estriction {M}onad for {N}ominal {S}ets and {C}pos},
   note = 	 {Unpublished notes for an invited talk given at CTCS},
   year = 	 {2004}