A Bidirectional Refinement Type System for LF. - William Lovas; Frank Pfenning (LFMTP@CADE, 2007)

Refinement Types as Proof Irrelevance. - William Lovas; Frank Pfenning (TLCA, 2009)

Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance - William Lovas; Frank Pfenning (Log. Methods Comput. Sci., 2010)

Refinement Types for Logical Frameworks. - William Lovas (2010)