3 ms·
You can prove a merge sort correct with dependent types. However, a typed implementation of merge sort will arguably be more difficult to mold into a TimSort if
by iso-8859-1 7y ago
You can prove a merge sort correct with dependent types. However, a typed implementation of merge sort will arguably be more difficult to mold into a TimSort if it isn't dependently typed. What you say?
- chongli 7y agoI don't have any experience with dependently typed languages. I hope (schedule permitting) to take a course in dependently typed programming (using Agda) and formal verification in the fall. I'll have much more to say on the topic after completing the course.