Skip navigation
Skip navigation

Machine-checked reasoning about complex voting schemes using higher-order logic

Dawson, Jeremy; Gore, Rajeev; Meumann, Tom


We describe how we first formally encoded the Englishlanguage Parliamentary Act for the Hare-Clark Single Transferable Vote-counting scheme used in the Australian state of Tasmania into higher-order logic, producing SPECHOL. Based on this logical specification, we then encoded an SML program to count ballots according to this specification inside the interactive theorem prover HOL4, giving us IMPHOL. We then manually transliterated the program as a real SML program IMP. We are currently...[Show more]

CollectionsANU Research Publications
Date published: 2015
Type: Conference paper
Source: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI: 10.1007/978-3-319-22270-7_9


File Description SizeFormat Image
01_Dawson_Machine-checked_reasoning_2015.pdf318.99 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator