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