1 Programming, Logic and Semantics, Software & Systems, The Department2 Theoretical Computer Science, The Department3 Process and System Models, Software & Systems, The Department4 Programming Logic and Semantics, Theoretical Computer Science, The Department5 Computer Science, IT University of Copenhagen6 Carnegie Mellon University7 Carnegie Mellon University
Current approaches to electronic implementations of voting protocols involve translating legal text to source code of an imperative programming language. Because the gap between legal text and source code is very large, it is difficult to trust that the program meets its legal specification. In response, we promote linear logic as a high-level language for both specifying and implementing voting protocols. Our linear logical specifications of the single-winner first-past-the-post (SW- FPTP) and single transferable vote (STV) protocols demonstrate that this approach leads to concise implementations that closely correspond to their legal specification, thereby increasing trust.
Lecture Notes in Computer Science, 2012, Vol 7187, p. 53-70