@TechReport{Lovas08tr,
  author =      {William Lovas and Frank Pfenning},
  title =       {A Bidirectional Refinement Type System for {LF}},
  institution = {Department of Computer Science, Carnegie Mellon University},
  month =       {May},
  year =        {2008},
  number =      {CMU-CS-08-129},
}