| Description | Instant-runoff voting (IRV) is used around the world; however, there are not many verified impliementation. In this project, our goal is to implement a verified implementation and then use it audit elections around the world, e.g., Australia elects its parliamentarian for the lower house using IRV, Alaska recently used it but it was controversial because it didn't elect the Condorcet candidate (so basically there are some ballot profiles for which IRV fails the Condorcet criteria) [1, 2], etc. You will prove that IRV fails on Condorcet and Monotonicity criteria.
This project requires basic idea of logic and programming. You don't need to an expert in theorem proving because I am happy to help you along the way. However, if you still don't feel comfortable, we can find out something intermediate, e.g., implementing it in Haskell and establishing some of its properties by property based testing library QuickCheck.
[1] https://www.tandfonline.com/doi/pdf/10.1080/10724117.2023.2224675
[2] https://arxiv.org/pdf/2303.00108v2 |
|---|