diff -r 8bda1d947df3 -r 603a36f19bfe LMCS-Paper/document/root.bib --- 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}