bib.bib

@inproceedings{PalmskogPGPR:2019,
	Author = {Karl Palmskog and Milos Gligoric and Lucas Pena and Grigore Ro\c{s}u},
	Booktitle = {The Fifth International Workshop on Coq for Programming Languages (CoqPL'19)},
	Date-Added = {2020-01-10 11:29:44 -0600},
	Date-Modified = {2020-01-10 11:51:40 -0600},
	Month = {January},
	Title = {Verifying Finality for Blockchain Systems},
	Year = {2019}
}

@techreport{PalmskogPGPMR:2018,
	Address = {http://hdl.handle.net/2142/102075},
	Author = {Karl Palmskog and Milos Gligoric and Lucas Pena and Brandon Moore and Grigore Ro\c{s}u},
	Date-Added = {2020-06-25 19:07:13 -0500},
	Date-Modified = {2020-06-25 19:11:53 -0500},
	Institution = {University of Illinois at Urbana-Champaign},
	Month = {November},
	Title = {Verification of {Casper} in the {Coq} Proof Assistant},
	Year = {2018}}

@misc{CasperProofs,
  title = {{Casper Proofs}},
  url = {https://github.com/runtimeverification/casper-proofs},
  year= {2018},
}

@misc{Eth2Specs,
  title = {{Ethereum 2.0 Specifications}},
  url = {https://github.com/ethereum/eth2.0-specs},
  year= {2020},
}

@misc{ButerinBHKPQRSWZ:2020,
	Archiveprefix = {arXiv},
	Author = {Vitalik Buterin and Diego Hernandez and Thor Kamphefner and Khiem Pham and Zhi Qiao and Danny Ryan and Juhyeok Sin and Ying Wang and Yan X Zhang},
	Date-Added = {2020-06-25 18:33:35 -0500},
	Date-Modified = {2020-06-25 18:34:00 -0500},
	Eprint = {2003.03052},
	Primaryclass = {cs.CR},
	Title = {Combining {GHOST} and {Casper}},
	Year = {2020}}

@inproceedings{Pirlea2018,
  author    = {George P{\^{\i}}rlea and
               Ilya Sergey},
  title     = {Mechanising blockchain consensus},
  booktitle = {Certified Programs and Proofs},
  pages     = {78--90},
  year      = {2018},
}

@article{Buterin2017,
  author    = {Vitalik Buterin and
               Virgil Griffith},
  title     = {Casper the Friendly Finality Gadget},
  journal   = {CoRR},
  volume    = {abs/1710.09437},
  year      = {2017}
}

@misc{Nakamoto2008,
    author = {Nakamoto, Satoshi},
    url = {http://www.bitcoin.org/bitcoin.pdf},
    title = {{Bitcoin: A peer-to-peer electronic cash system}},
    year = {2008}
}

@article{Wood2014,
  title={Ethereum: A secure decentralised generalised transaction ledger},
  author={Wood, Gavin},
  year = 2014,
  url = {http://gavwood.com/paper.pdf},
}

@misc{Toychain,
    url = {https://github.com/certichain/toychain},
    title = {Toychain},
    year = {2018},
}

@misc{CasperToychain,
    url = {https://github.com/palmskog/caspertoychain/},
    title = {{Casper Toychain}},
    year = {2018},
}

@misc{Bitoychain,
 url = {https://github.com/palmskog/bitoychain},
 title = {Bitoychain},
 year = {2018},
}

@Article{Czajka2018,
author="Czajka, {\L}ukasz
and Kaliszyk, Cezary",
title="Hammer for {Coq}: Automation for Dependent Type Theory",
journal="Journal of Automated Reasoning",
year="2018",
LONGmonth="Jun",
LONGday="01",
volume="61",
number="1",
pages="423--453",
LONGissn="1573-0670",
LONGdoi="10.1007/s10817-018-9458-4",
LONGurl="https://doi.org/10.1007/s10817-018-9458-4"
}

@misc{CoqHammer,
 url = {https://github.com/lukaszcz/coqhammer},
 title = {CoqHammer},
 year = {2018},
}

@misc{pos,
 url = {https://github.com/palmskog/pos},
 author = {Yoichi Hirai},
 title = {A repository for {PoS} related formal methods},
 year = {2018},
}

@inproceedings{Woos2016,
 author = {Woos, Doug and Wilcox, James R. and Anton, Steve and Tatlock, Zachary and Ernst, Michael D. and Anderson, Thomas},
 title = {Planning for Change in a Formal Verification of the {Raft} Consensus Protocol},
 booktitle = {CPP},
 year = {2016},
 pages = {154--165},
 LONGurl = {http://doi.acm.org/10.1145/2854065.2854081},
 LONGdoi = {10.1145/2854065.2854081},
 LONGaddress = {New York, NY, USA},
}

@article{Appel2017,
  author = {Appel, Andrew W. and Beringer, Lennart and Chlipala, Adam and Pierce, Benjamin C. and Shao, Zhong and Weirich, Stephanie and Zdancewic, Steve},
  title = {Position paper: the science of deep specification},
  volume = {375},
  number = {2104},
  year = {2017},
  LONGdoi = {10.1098/rsta.2016.0331},
  LONGpublisher = {The Royal Society},
  LONGissn = {1364-503X},
  journal = {Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences}
}

@misc{MathComp,
  title = {Mathematical Components Project},
  url = {https://math-comp.github.io/math-comp/},
  year= {2020},
}

@Article{Ballarin2014,
author="Ballarin, Clemens",
title="Locales: A Module System for Mathematical Theories",
journal="Journal of Automated Reasoning",
year="2014",
month="Feb",
day="01",
volume="52",
number="2",
pages="123--153",
LONGissn="1573-0670",
LONGdoi="10.1007/s10817-013-9284-7",
LONGurl="https://doi.org/10.1007/s10817-013-9284-7"
}

@misc{Beacon,
  title = {{Beacon Chain}},
  url = {https://github.com/ethereum/eth2.0-specs/blob/dev/specs/phase0/beacon-chain.md},
  year= {2020},
}

@misc{CasperToychain,
  title = {{Casper Toychain}},
  url = {https://github.com/palmskog/caspertoychain},
  year= {2018},
}

@misc{fcslpcm,
  title = {{PCM} library},
  url = {https://github.com/imdea-software/fcsl-pcm},
  year= {2018},
}

@misc{sharding,
  title = {Sharding {FAQs}},
  url = {https://github.com/ethereum/wiki/wiki/Sharding-FAQs},
  year= {2018},
}

@inproceedings{Garillot2009,
  author = "Garillot, Fran{\c{c}}ois and Gonthier, Georges and Mahboubi, Assia and Rideau, Laurence",
  title = {Packaging Mathematical Structures},
  booktitle = "Theorem Proving in Higher Order Logics",
  year = "2009",
  LONGpublisher = "Springer Berlin Heidelberg",
  LONGaddress = "Berlin, Heidelberg",
  pages = {327--342},
}

@Inproceedings{Gonthier2013,
author="Gonthier, Georges
and Asperti, Andrea
and Avigad, Jeremy
and Bertot, Yves
and Cohen, Cyril
and Garillot, Fran{\c{c}}ois
and Le Roux, St{\'e}phane
and Mahboubi, Assia
and O'Connor, Russell
and Ould Biha, Sidi
and Pasca, Ioana
and Rideau, Laurence
and Solovyev, Alexey
and Tassi, Enrico
and Th{\'e}ry, Laurent",
LONGeditor="Blazy, Sandrine
and Paulin-Mohring, Christine
and Pichardie, David",
title="A Machine-Checked Proof of the Odd Order Theorem",
bookTitle="Interactive Theorem Proving",
year="2013",
LONGpublisher="Springer Berlin Heidelberg",
LONGaddress="Berlin, Heidelberg",
pages="163--179",
LONGisbn="978-3-642-39634-2",
LONGdoi="10.1007/978-3-642-39634-2_14",
}

@Inproceedings{Bertot2008,
author="Bertot, Yves
and Gonthier, Georges
and Ould Biha, Sidi
and Pasca, Ioana",
LONGeditor="Mohamed, Otmane Ait
and Mu{\~{n}}oz, C{\'e}sar
and Tahar, Sofi{\`e}ne",
title="Canonical Big Operators",
bookTitle="Theorem Proving in Higher Order Logics",
year="2008",
LONGpublisher="Springer",
LONGaddress="Berlin, Germany",
pages="86--101",
LONGisbn="978-3-540-71067-7",
doi="10.1007/978-3-540-71067-7_11",
LONGurl="https://doi.org/10.1007/978-3-540-71067-7_11",
}

@InProceedings{proof-of-stake,
author="Bentov, Iddo
and Gabizon, Ariel
and Mizrahi, Alex",
editor="Clark, Jeremy
and Meiklejohn, Sarah
and Ryan, Peter Y.A.
and Wallach, Dan
and Brenner, Michael
and Rohloff, Kurt",
title="Cryptocurrencies Without Proof of Work",
booktitle="Financial Cryptography and Data Security",
year="2016",
publisher="Springer",
address="Berlin, Heidelberg",
pages="142--157",
isbn="978-3-662-53357-4"
}

@misc{EthereumGrant2018,
  author = {{Ethereum Team}},
  title = {Announcing Beneficiaries of the Ethereum Foundation Grants},
  url = {https://blog.ethereum.org/2018/03/07/announcing-beneficiaries-ethereum-foundation-grants/},
  year = {2018},
}