Logic and Computation Group

Electronic Voting - Formalisation of the ACT Hare-Clark Legislation

We have converted the English specification of the Hare-Clark method given in the Electoral Act 1992 into a logical specification which is mechanically manipulable by the HOL theorem prover. This mechanisation has two advantages:

• We now have a reference specification against which the family of implementations we are working on can be verified.
• The logic used in HOL is sufficiently similar to the programming language ML that an ML implementation of the specification should be easy to derive in at least a semi-automatic fashion.

The current specification is available as a PDF file.