I'm interested in applicability of refinement types to theorem-proving hence the questions about their logical expressiveness. Let's say, we have a type system which corresponds to some logic according to Curry-Howard isomorphism.

  1. How is the expressiveness of the logic affected by refining the system with predicates? If refinement predicates can belong to a different logic than that of the underlying system, what influence may it have on the original logic?
  2. How is the choice of the logic for refinement predicates motivated in real systems such as LiquidHaskell?
  3. How close can we get to higher order logic with refinement types?
  • 1
    $\begingroup$ Regarding (2) a constraint that people care about is decidability, which probably limits to how 'close' you can get to higher-order logic. Ideally, we'd also like refinement types to be sound, which has sometimes proven tricky: the classical translation of refinement types to verification conditions is unsound under lazy evaluation. $\endgroup$ Feb 12, 2021 at 15:41
  • $\begingroup$ @MartinBerger thanks! Can you point me to an explanation of the unsoundness issue? $\endgroup$
    – oquechy
    Feb 13, 2021 at 16:08
  • 1
    $\begingroup$ It's a bit difficult, because the unsoundness bugs have not been made as easily accessible as one would hope ... How about Functional Extensionality for Refinement Types? $\endgroup$ Feb 13, 2021 at 16:58


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.