{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:28Z","timestamp":1740099148460,"version":"3.37.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030004187"},{"type":"electronic","value":"9783030004194"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00419-4_4","type":"book-chapter","created":{"date-parts":[[2018,9,5]],"date-time":"2018-09-05T01:35:09Z","timestamp":1536111309000},"page":"51-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Modular Formalisation and Verification of STV Algorithms"],"prefix":"10.1007","author":[{"given":"Milad K.","family":"Ghale","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dirk","family":"Pattinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mukesh","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,6]]},"reference":[{"key":"4_CR1","unstructured":"ACT Electoral Commission: https:\/\/www.elections.act.gov.au\/education\/act_electoral_commission_fact_sheets\/fact_sheets_-_general_html\/elections_act_factsheet_hare-clark_electoral_system"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-38574-2_9","volume-title":"Automated Deduction \u2013 CADE-24","author":"B Beckert","year":"2013","unstructured":"Beckert, B., Gor\u00e9, R., Sch\u00fcrmann, C.: Analysing vote counting algorithms via logic - and its application to the CADE election scheme. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 135\u2013144. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_9"},{"key":"4_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P., Huet, G., Paulin-Mohring, C.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Cortier, V., Galindo, D., K\u00fcsters, R., M\u00fcller, J., Truderung, T.: Verifiability notions for e-voting protocols. IACR Cryptology ePrint Archive 2016, 287 (2016)","DOI":"10.1109\/SP.2016.52"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Dawson, J.E., Gor\u00e9, R., Meumann, T.: Machine-checked reasoning about complex voting schemes using higher-order logic. In: Proceedings of EVote-ID 2015, pp. 142\u2013158 (2015)","DOI":"10.1007\/978-3-319-22270-7_9"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-32747-6_4","volume-title":"E-Voting and Identity","author":"H DeYoung","year":"2012","unstructured":"DeYoung, H., Sch\u00fcrmann, C.: Linear logical voting protocols. In: Kiayias, A., Lipmaa, H. (eds.) Vote-ID 2011. LNCS, vol. 7187, pp. 53\u201370. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32747-6_4"},{"issue":"2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"141","DOI":"10.2307\/2339223","volume":"44","author":"HR Droop","year":"1881","unstructured":"Droop, H.R.: On methods of electing representatives. J. Stat. Soc. Lond. 44(2), 141\u2013202 (1881)","journal-title":"J. Stat. Soc. Lond."},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-319-68687-5_10","volume-title":"Electronic Voting","author":"MK Ghale","year":"2017","unstructured":"Ghale, M.K., Gor\u00e9, R., Pattinson, D.: A formally verified single transferable voting scheme with fractional values. In: Krimmer, R., Volkamer, M., Braun Binder, N., Kersting, N., Pereira, O., Sch\u00fcrmann, C. (eds.) E-Vote-ID 2017. LNCS, vol. 10615, pp. 163\u2013182. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68687-5_10"},{"issue":"3","key":"4_CR9","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","volume":"59","author":"J Girard","year":"1993","unstructured":"Girard, J.: On the unity of logic. Ann. Pure Appl. Logic 59(3), 201\u2013217 (1993)","journal-title":"Ann. Pure Appl. Logic"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-52240-1_9","volume-title":"Electronic Voting","author":"R Gor\u00e9","year":"2017","unstructured":"Gor\u00e9, R., Lebedeva, E.: Simulating STV hand-counting by computers considered harmful: A.C.T. In: Krimmer, R., et al. (eds.) E-Vote-ID 2016. LNCS, vol. 10141, pp. 144\u2013163. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52240-1_9"},{"key":"4_CR11","unstructured":"John Muir Trust: Apply to be a trustee. https:\/\/www.johnmuirtrust.org\/assets\/000\/002\/860\/How_to_apply_to_be_a_Trustee_Jan_2018_original.pdf . Accessed 15 May 2018"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Principles of Programming Languages (POPL). ACM, January 2014","DOI":"10.1145\/2535838.2535841"},{"issue":"2\u20133","key":"4_CR13","first-page":"284","volume":"24","author":"MO Magnus","year":"2014","unstructured":"Magnus, M.O., Scott, O.: Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2\u20133), 284\u2013315 (2014)","journal-title":"J. Funct. Program."},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for CoQ. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200\u2013219. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-39185-1_12"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-319-26350-2_41","volume-title":"AI 2015: Advances in Artificial Intelligence","author":"D Pattinson","year":"2015","unstructured":"Pattinson, D., Sch\u00fcrmann, C.: Vote counting as mathematical proof. In: Pfahringer, B., Renz, J. (eds.) AI 2015. LNCS (LNAI), vol. 9457, pp. 464\u2013475. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26350-2_41"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-319-66107-0_26","volume-title":"Interactive Theorem Proving","author":"D Pattinson","year":"2017","unstructured":"Pattinson, D., Tiwari, M.: Schulze voting as evidence carrying computation. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 410\u2013426. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_26"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Schack-Nielsen, A., Sch\u00fcrmann, C.: Celf - a logical framework for deductive and concurrent systems (system description). In: Proceedings of IJCAR 2008, pp. 320\u2013326 (2008)","DOI":"10.1007\/978-3-540-71070-7_28"},{"key":"4_CR18","unstructured":"Software Improvements: Electronic and voting and counting sytems. http:\/\/www.softimp.com.au\/evacs\/index.html . Accessed 12 May 2015"},{"key":"4_CR19","unstructured":"StackExchange: Moderator elections (2018). https:\/\/math.stackexchange.com\/election\/6?tab=election . Accessed 15 May 2018"},{"key":"4_CR20","unstructured":"The Parliament of Victoria: Electoral act 2002. http:\/\/www.legislation.vic.gov.au\/domino\/web_notes\/ldms\/pubstatbook.nsf\/f932b66241ecf1b7ca256e92000e23be\/3264bf1de203c08aca256e5b00213ffb\/%24FILE\/02-023a.pdf"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Verity, F., Pattinson, D.: Formally verified invariants of vote counting schemes. In: Proceedings of ACSW 2017, pp. 31:1\u201331:10 (2017)","DOI":"10.1145\/3014812.3014845"}],"container-title":["Lecture Notes in Computer Science","Electronic Voting"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00419-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T12:54:48Z","timestamp":1571835288000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00419-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030004187","9783030004194"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00419-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}