| Description | Single Transferable Voting (STV) [1, 3] is used around the world, e.g., Australia , Local Councils of Wales [2], Ireland, etc. The goal of this project is to implement it in Coq, Lean, or Dafny and prove that its correctness properties, e.g., it does not follow Condorcet criteria, etc.
This project requires basic understanding of logic and programming but you don't need to an expert. However, if you still feel unsure we can talk and figure out some middle way, e.g., implementing in Haskell, or OCaml and use property based testing to establish some of the properties.
[1] https://en.wikipedia.org/wiki/Single_transferable_vote
[2] https://www.gov.wales/consultation-draft-rules-local-government-principal-council-elections-using-single-transferable
[3] https://www.electoral-reform.org.uk/voting-systems/types-of-voting-system/single-transferable-vote/ |
|---|