Schulze voting as evidence carrying computation

DOI10.1007/978-3-319-66107-0_26zbMath1484.68317OpenAlexW2745320640MaRDI QIDQ1687758

Dirk Pattinson, Mukesh Tiwari

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_26

Mathematics Subject Classification ID

Voting theory (91B12) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Coq
• CakeML

Cites Work

• Schulze and ranked-pairs voting are fixed-parameter tractable to bribe, manipulate, and control
• A new monotonic, clone-independent, reversal symmetric, and condorcet-consistent single-winner election method
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A lattice-theoretical fixpoint theorem and its applications
• Extraction in Coq: An Overview
• CakeML
• An Algebra for Network Routing Problems
• Unnamed Item

This page was built for publication: Schulze voting as evidence carrying computation