Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance (Logical Methods in Computer Science, 2010)