@inproceedings{Lovas09subset,
  author =      {William Lovas and Frank Pfenning},
  title =       {Refinement Types as Proof Irrelevance},
  booktitle =   {Proceedings of 9th International Conference on Typed Lambda
                 Calculi and Applications (TLCA 2009)},
  editor =      {Pierre-Louis Curien},
  series =      {Lecture Notes in Computer Science},
  number =      {5608},
  pages =       {157--171},
  year =        {2009},
  publisher =   {Springer},
}