The general binary search algorithm described here by Jules Jacobs is more flexible and is simpler to formally verify than the traditional presentation. Here, we implement and verify its correctness using the Lean programming language and theorem prover.
-
Notifications
You must be signed in to change notification settings - Fork 0
jjakpor/binary-search
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
A Lean formalization of the general binary search algorithm.
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published