<p>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.</p>
<ol>
<li>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?</li>
<li>How is the choice of the logic for refinement predicates motivated in real systems such as LiquidHaskell?</li>
<li>How close can we get to higher order logic with refinement types?</li>
</ol>

CC BY-SA 4.0
2021-02-12T15:41:49.910Z
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.
Martin Berger
CC BY-SA 4.0
2021-02-13T16:08:35.560Z
@MartinBerger thanks! Can you point me to an explanation of the unsoundness issue?
oquechy
CC BY-SA 4.0
2021-02-13T16:58:28.670Z
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](https://cs.pomona.edu/~michael/papers/2020_lh_funext.pdf)?
Martin Berger
<type-theory><dependent-type><automated-theorem-proving><curry-howard>
What logic do refinement types correspond to?
oquechy
# What logic do refinement types correspond to?

(Asked by: username_0 on 2021-02-12)

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?

**Tags:** type-theory, dependent-type, automated-theorem-proving, curry-howard

> **Comments:**
> **username_1**: 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.  
> **username_0**: @MartinBerger thanks! Can you point me to an explanation of the unsoundness issue?  
> **username_1**: 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](https://cs.pomona.edu/~michael/papers/2020_lh_funext.pdf)?  

---

## 0 answers

