Questions tagged [f-star]

F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification.

Filter by
Sorted by
Tagged with
9 votes
2 answers
342 views

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

In the F* proof assistant, they use refinement types together with dependent types. Based on my impression of F*, it seems to me that refinement types are just predicates in dependent type theory that ...