@article{Lovas07,
  author =      {William Lovas and Frank Pfenning},
  title =       {A Bidirectional Refinement Type System for {LF}},
  journal =     {Electronic Notes in Theoretical Computer Science},
  volume =      {196},
  month =       {January},
  year =        {2008},
  pages =       {113--128}
  keywords =    {LF, refinement types, subtyping, dependent types, intersection types},
  ee =          {http://dx.doi.org/10.1016/j.entcs.2007.09.021}
  urlpdf =      {http://www.cs.cmu.edu/~wlovas/papers/lfr.pdf}
}