Skip to main content
11 votes
Accepted

What's the relationship between refinement types and dependent types?

Is there something that is only possible with refinement types, but not possible (or extremely hard to imitate) in dependent types? Yes. Refinement types make the notion of logical or ghost term ...
Neel Krishnaswami's user avatar
8 votes

What's the relationship between refinement types and dependent types?

I am not sure that there is a unique definition of refinement types, but there is a common theme. In general, a system featuring refinement types is some kind of ML extended with a subset type ...
Pierre-Marie Pédrot's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible