@inproceedings{ca6bb090c15d42799c130698c20af873,
title = "A formally verified single transferable voting scheme with fractional values",
abstract = "We formalise a variant of the Single Transferable Vote scheme with fractional transfer values in the theorem prover Coq. Our method advocates the idea of vote counting as application of a sequence of rules. The rules are an intermediate step for specifying the protocol for vote-counting in a precise symbolic language. We then formalise these rules in Coq. This reduces the gap between the legislation and formalisation so that, without knowledge of formal methods, one can still validate the process. Moreover our encoding is modular which enables us to capture other Single Transferable Vote schemes without significant changes. Using the built-in extraction mechanism of Coq, a Haskell program is extracted automatically. This program is guaranteed to meet its specification. Each run of the program outputs a certificate which is a precise, independently checkable record of the trace of computation and provides all relevant details of how the final result is obtained. This establishes correctness, reliability, and verifiability of the count.",
author = "Ghale, {Milad K.} and Rajeev Gor{\'e} and Dirk Pattinson",
note = "Publisher Copyright: {\textcopyright} 2017, Springer International Publishing AG.; 2nd International Joint Conference on Electronic Voting, E-Vote-ID 2017 ; Conference date: 24-10-2017 Through 27-10-2017",
year = "2017",
doi = "10.1007/978-3-319-68687-5_10",
language = "English",
isbn = "9783319686868",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "163--182",
editor = "Melanie Volkamer and Olivier Pereira and Robert Krimmer and Norbert Kersting and Carsten Schurmann and {Braun Binder}, Nadja",
booktitle = "Electronic Voting - 2nd International Joint Conference, E-Vote-ID 2017, Proceedings",
address = "Germany",
}