Questions tagged [f-star]
F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification.
1
question
9
votes
2
answers
300
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 ...