Simplicity.bib

@incollection{gentzen,
  author={Gentzen, G.},
  title={Investigations into Logical Deduction},
  booktitle={The collected papers of Gerhard Gentzen},
  editor={Szabo, M.E.},
  chapter=3,
  series={Studies in logic and the foundations of mathematics},
  year={1969},
  publisher={North-Holland Pub. Co.}
}

@misc{appel,
  author       = {Appel, A. W.},
  title        = {Verifiable {C}},
  howpublished = "\url{http://vst.cs.princeton.edu/download/VC.pdf}",
  month        = Jul,
  year         = 2016,
}

@misc{goldfederescrow,
  title={Escrow protocols for cryptocurrencies: How to buy physical goods using Bitcoin},
  author={Goldfeder, S. and Bonneau, J. and Gennaro, R. and Narayanan, A.},
  howpublished = "\url{http://fc17.ifca.ai/preproceedings/paper_122.pdf}",
  month        = Apr,
  year         = 2017,
  note = "To appear in the proceedings of the 21st International Conference on Financial Cryptography and Data Security"
}

@article{Appel:2015,
 author = {Appel, A. W.},
 title = {Verification of a Cryptographic Primitive: {SHA-256}},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {April 2015},
 volume = {37},
 number = {2},
 month = apr,
 year = {2015},
 issn = {0164-0925},
 pages = {7:1--7:31},
 articleno = {7},
 numpages = {31},
 url = {http://doi.acm.org/10.1145/2701415},
 doi = {10.1145/2701415},
 acmid = {2701415},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Cryptography},
}

@article{unification,
title = "Linear unification",
journal = "Journal of Computer and System Sciences",
volume = "16",
number = "2",
pages = "158 - 167",
year = "1978",
note = "",
issn = "0022-0000",
doi = "http://dx.doi.org/10.1016/0022-0000(78)90043-0",
url = "http://www.sciencedirect.com/science/article/pii/0022000078900430",
author = "M. S. Paterson and M. N. Wegman",

}

@techreport{sec2,
author = 	"{Certicom Research}",
title = 	"{Standards for Efficient Cryptography 2: Recommended Elliptic Curve Domain Parameters}",
institution = 	"Certicom Corp.",
year = 		2000,
type = 		"Standard",
number = 	"SEC2",
address = 	"Mississauga, ON, USA",
month = 	Sep
}

@manual{Coq:manual,
  author = {{Coq} {Development} {Team}, The},
  title  = {The {Coq} Proof Assistant Reference Manual, version 8.7},
  month  = Oct,
  year   = {2017},
  url    = {http://coq.inria.fr}
}

@misc{oconnor2014,
  author	= "O'Connor, R.",
  title		= {{van Laarhoven} Free Monad},
  year		= 2014,
  month     = Feb,
  day       = 02,
  note		= {Blog post, \url{http://r6.ca/blog/20140210T181244Z.html}}
}

@MISC{script,
    author = {bitcoinwiki},
    title = {Script},
    howpublished = "\url{https://en.bitcoin.it/w/index.php?title=Script&oldid=61707}",
    year = {2016}
}

@misc{sighash,
  author	= "Bitcoin Developer Guide",
  title		= {Signature Hash Types},
  note		= "\url{https://bitcoin.org/en/developer-guide\string#signature-hash-types}",
  year = {2014}
}

@MISC{bitcoin,
    author = {Nakamoto, S.},
    title = {{Bitcoin: A peer-to-peer electronic cash system}},
    howpublished = "\url{http://bitcoin.org/bitcoin.pdf}",
    month = Nov,
    year = {2008}
}

@misc{libsecp256k1,
    author = "Wuille, P.",
    title = {{libsecp256k1}},
    howpublished = "\url{https://github.com/bitcoin-core/secp256k1/tree/1e6f1f5ad5e7f1e3ef79313ec02023902bf8175c}",
    month = May,
    year = {2018},
}

@misc{misc,
    author = {Nakamoto, S.},
    title = {{misc changes}},
    howpublished = "\url{https://github.com/bitcoin/bitcoin/commit/4bd188c4383d6e614e18f79dc337fbabe8464c82}",
    month = Aug,
    year = {2010},
    note = "\url{https://bitcoin.svn.sourceforge.net/svnroot/bitcoin/trunk@131}"
}

@misc{satoshiScript,
    author = {Nakamoto, S.},
    title = {{Re: Transactions and Scripts: DUP HASH160 ... EQUALVERIFY CHECKSIG}},
    howpublished = "\url{https://bitcointalk.org/index.php?topic=195.msg1611\string#msg1611}",
    month = Jun,
    year = {2010},
}


@misc{sidechains,
  author	= "Back, A. and Corallo, M. and Dashjr, L. and Friedenbach, M. and Maxwell, G. and Miller, A. and Poelstra, A. and Tim\'on, J. and Wuille, P.",
  title		= "Enabling Blockchain Innovations with Pegged Sidechains",
  year		= 2014,
  note		= "\url{https://www.blockstream.com/sidechains.pdf}"
}

@misc{andresen2012-2,
  author	= "Andresen, G.",
  howpublished	= "{Bitcoin} Improvement Proposal",
  title		= "{BIP16}: Pay to Script Hash",
  note		= "\url{https://github.com/bitcoin/bips/blob/master/bip-0016.mediawiki}",
  year		= 2012
}

@misc{cltv,
  author	= "Todd, P.",
  howpublished	= "{Bitcoin} Improvement Proposal",
  title		= "{BIP65}: OP\_CHECKLOCKTIMEVERIFY",
  note		= "\url{https://github.com/bitcoin/bips/blob/master/bip-0065.mediawiki}",
  year		= 2014
}

@misc{mast,
  author	= "Lau, J.",
  howpublished	= "{Bitcoin} Improvement Proposal",
  title		= "{BIP114}: Merkelized Abstract Syntax Tree",
  note		= "\url{https://github.com/bitcoin/bips/blob/master/bip-0114.mediawiki}",
  year		= 2016
}

@misc{csv,
  author	= "BtcDrak and Friedenbach, M. and Lombrozo, E.",
  howpublished	= "{Bitcoin} Improvement Proposal",
  title		= "{BIP112}: CHECKSEQUENCEVERIFY",
  note		= "\url{https://github.com/bitcoin/bips/blob/master/bip-0112.mediawiki}",
  year		= 2015
}

@misc{bip-0340,
  author	= "Wuille, P. and Nick, J. and Ruffing, T.",
  title		= "bip-0340",
  note		= "\url{https://github.com/bitcoin/bips/blob/master/bip-0340.mediawiki}",
  year		= 2020
}

@misc{zkcp,
  author	= "Maxwell, G.",
  title		= {Zero-Knowledge Contingent Payment},
  year		= 2011,
  note		= "\url{https://en.bitcoin.it/wiki/Zero\_Knowledge\_Contingent\_Payment}"
}

@misc{urbit,
  author	= "Yarvin, C. and Monk, P. and Dyudin, A. and Pasco, R.",
  title		= {Urbit: A Solid-State Interpreter},
  month     = May,
  year		= 2016,
  note		= "\url{http://media.urbit.org/whitepaper.pdf}"
}

@article{compcert,
  author = {Leroy, X.},
  title = {Formal verification of a realistic compiler},
  journal = {Communications of the ACM},
  year = 2009,
  volume = 52,
  number = 7,
  pages = {107--115},
  url = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
  pubkind = {journal-int-mono},
  abstract = {This paper reports on the development and formal verification (proof
of semantic preservation) of CompCert, a compiler from Clight (a
large subset of the C programming language) to PowerPC assembly code,
using the Coq proof assistant both for programming the compiler and
for proving its correctness.  Such a verified compiler is useful in
the context of critical software and its formal verification: the
verification of the compiler guarantees that the safety properties
proved on the source code hold for the executable compiled code as
well.}
}


@inproceedings{schnorr1989,
  author        = "Schnorr, C. P.",
  title         = "Efficient Identification and Signatures for Smart Cards",
  booktitle     = {Proceedings of CRYPTO '89},
  year          = 1989,
}

@article{ecdsa,
    author = {{National institute of standards and technology}},
    title = {{FIPS} Pub 186-4 Federal Information Processing Standards Publication Digital Signature Standard (DSS)},
    url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.362.5590},
    year = {2013}
}

@techreport{sha,
    author = {{National institute of standards and technology}},
    day = {26},
    institution = {DEPARTMENT OF COMMERCE},
    keywords = {cryptography, hash, standard},
    month = aug,
    title = {{FIPS} 180-4, Secure Hash Standard, Federal Information Processing Standard ({FIPS}), Publication 180-4},
    url = {http://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf},
    year = {2015}
}

@misc{oconnor2016,
  author	= "O'Connor, R.",
  title		= {Covenants in Elements Alpha},
  year		= 2016,
  note		= {Blog post, \url{https://blockstream.com/2016/11/02/covenants-in-elements-alpha.html}}
}

@Inbook{King1993,
author="King, D. J. and Wadler, P.",
editor="Launchbury, John and Sansom, Patrick",
title="Combining Monads",
bookTitle="Functional Programming, Glasgow 1992: Proceedings of the 1992 Glasgow Workshop on Functional Programming, Ayr, Scotland, 6--8 July 1992",
year="1993",
publisher="Springer London",
address="London",
pages="134--143",
abstract="Monads provide a way of structuring functional programs. Most real applications require a combination of primitive monads. Here we describe how some monads may be combined with others to yield a combined monad.",
isbn="978-1-4471-3215-8",
doi="10.1007/978-1-4471-3215-8_12",
url="https://doi.org/10.1007/978-1-4471-3215-8_12"
}

@inproceedings{Mairson:1989,
 author = {Mairson, H. G.},
 title = {Deciding {ML} Typability is Complete for Deterministic Exponential Time},
 booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '90},
 year = {1990},
 isbn = {0-89791-343-4},
 location = {San Francisco, California, USA},
 pages = {382--401},
 numpages = {20},
 url = {http://doi.acm.org/10.1145/96709.96748},
 doi = {10.1145/96709.96748},
 acmid = {96748},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@article{Carette:2009,
 author = {Carette, J. and Kiselyov, O. and Shan, C.},
 title = {Finally Tagless, Partially Evaluated: Tagless Staged Interpreters for Simpler Typed Languages},
 journal = {J. Funct. Program.},
 issue_date = {September 2009},
 volume = {19},
 number = {5},
 month = sep,
 year = {2009},
 issn = {0956-7968},
 pages = {509--543},
 numpages = {35},
 url = {http://dx.doi.org/10.1017/S0956796809007205},
 doi = {10.1017/S0956796809007205},
 acmid = {1630626},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}

@inproceedings{Mahboubi:2013,
 author = {Mahboubi, A. and Tassi, E.},
 title = {Canonical Structures for the Working {Coq} User},
 booktitle = {Proceedings of the 4th International Conference on Interactive Theorem Proving},
 series = {ITP'13},
 year = {2013},
 isbn = {978-3-642-39633-5},
 location = {Rennes, France},
 pages = {19--34},
 numpages = {16},
 url = {http://dx.doi.org/10.1007/978-3-642-39634-2_5},
 doi = {10.1007/978-3-642-39634-2_5},
 acmid = {2529322},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@inproceedings{garillot:2009,
  TITLE = {{Packaging Mathematical Structures}},
  AUTHOR = {Garillot, F. and Gonthier, G. and Mahboubi, A. and Rideau, L.},
  URL = {https://hal.inria.fr/inria-00368403},
  BOOKTITLE = {{Theorem Proving in Higher Order Logics}},
  ADDRESS = {Munich, Germany},
  EDITOR = {Tobias Nipkow and Christian Urban},
  PUBLISHER = {{Springer}},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {5674},
  YEAR = {2009},
  KEYWORDS = {Formalization of Algebra ; Coercive subtyping ; Type inference ; Coq ; SSReflect},
  PDF = {https://hal.inria.fr/inria-00368403/file/main.pdf},
  HAL_ID = {inria-00368403},
  HAL_VERSION = {v2},
}

@misc{f-algebra,
    author = "{Wikipedia contributors}",
    title = "F-algebra --- {Wikipedia}{,} The Free Encyclopedia",
    year = "2017",
    howpublished = "\url{https://en.wikipedia.org/w/index.php?title=F-algebra&oldid=814231684}",
  }