TY - RPRT TI - Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance AU - William Lovas AU - Frank Pfenning PY - 2010 DO - 10.2168/lmcs-6(4:5)2010 UR - https://arxiv.org/abs/1009.1861 ID - 1009.1861 ER -