Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance

William Lovas, Frank Pfenning

Refinement types sharpen systems of simple and dependent types by offering expressive means to more precisely classify well-typed terms. We present a system of refinement types for…