@Article{hl07mechanizing,
  author = 	 {Robert Harper and Daniel R. Licata},
  title = 	 {Mechanizing Metatheory in a Logical Framework},
  journal = 	 {Journal of Functional Programming},
  year = 	 {2007},
  month =        {July},
  volume =       {17},
  number =       {4--5},
  pages  =       {613--673},
}