about
writing
Writing with tag
idris
Formally verifying insertion sort in Idris
May 24, 2026
15 min
idris
dependent-type
Using the dependently-typed programming language Idris to verify insertion sort.