@book{smith1776WealthOfNations,
  title={An {I}nquiry Into the {N}ature and {C}auses of the {W}ealth of {N}ations},
  author={Smith, A.},
  number={v. 1},
  series={An Inquiry Into the Nature and Causes of the Wealth of Nations},
  url={https://books.google.at/books?id=C5dNAAAAcAAJ},
  year={1776},
  publisher={Strahan}
}

@Book{RePEc:mtp:titles:0262571579,
  author={Victor Ginsburgh and Michiel Keyzer},
  title={{The Structure of Applied General Equilibrium Models}},
  publisher={The MIT Press},
  year=2002,
  month={July},
  volume={1},
  number={0262571579},
  series={MIT Press Books},
  keywords={general equilibrium; AGE modeling},
  isbn={0262071797},
  abstract={General equilibrium and AGE modeling are both active fields of research. Yet the applied model builder often finds the style of theoretical papers inaccessible, while the theoretician hardly recognizes the concepts used in the equations of applied models. The Structure of Applied General Equilibrium Models bridges that gap through a comprehensive analysis of the theoretical underpinnings of the applied models.},
  url={https://ideas.repec.org/b/mtp/titles/0262571579.html}
}

@Book{starr2011general,
  title={General Equilibrium Theory: An Introduction},
  author={Starr, R.M.},
  isbn={9781139496735},
  url={https://books.google.at/books?id=t9pSAlEMyDYC},
  year={2011},
  publisher={Cambridge University Press}
}

@book{rubinfeld:micro,
  Author = {Robert Pindyck and Daniel Rubinfeld},
  Title = {Microeconomics (8th Edition) (The Pearson Series in Economics)},
  Publisher = {Pearson},
  Year = {2012},
  ISBN = {013285712X},
}

@book{VarianMicroEcon,
  author    = {Hal R. Varian},
  title     = {Intermediate Microeconomics: A Modern Approach},
  publisher = "W. W. Norton \& Co Inc",
  year      = {2014},
  month     = {April},
  edition   = {9th},
  isbn      = {978-0-393-12396-8}
}

@article{FORNI2009559,
title = "The general equilibrium effects of fiscal policy: Estimates for the Euro area",
journal = "Journal of Public Economics",
volume = "93",
number = "3",
pages = "559 - 585",
year = "2009",
note = "",
issn = "0047-2727",
doi = "https://doi.org/10.1016/j.jpubeco.2008.09.010",
url = "http://www.sciencedirect.com/science/article/pii/S0047272708001382",
author = "Lorenzo Forni and Libero Monteforte and Luca Sessa",
keywords = "Fiscal policy",
keywords = "Distortionary taxation",
keywords = "DSGE modeling",
keywords = "Bayesian estimation"
}

@article{10.2307/1907353,
 ISSN = {00129682, 14680262},
 URL = {http://www.jstor.org/stable/1907353},
 abstract = {A. Wald has presented a model of production and a model of exchange and proofs of the existence of an equilibrium for each of them. Here proofs of the existence of an equilibrium are given for an integrated model of production, exchange and consumption. In addition the assumptions made on the technologies of producers and the tastes of consumers are significantly weaker than Wald's. Finally a simplification of the structure of the proofs has been made possible through use of the concept of an abstract economy, a generalization of that of a game.},
 author = {Kenneth J. Arrow and Gerard Debreu},
 journal = {Econometrica},
 number = {3},
 pages = {265-290},
 publisher = {[Wiley, Econometric Society]},
 title = {Existence of an Equilibrium for a Competitive Economy},
 volume = {22},
 year = {1954}
}


@article{10.2307/27648302,
 ISSN = {08953309},
 URL = {http://www.jstor.org/stable/27648302},
 author = {Roger E. Backhouse and Steven G. Medema},
 journal = {The Journal of Economic Perspectives},
 number = {1},
 pages = {221-234},
 publisher = {American Economic Association},
 title = {Retrospectives: On the Definition of Economics},
 volume = {23},
 year = {2009}
}

@book{essay:robbins,
author = {Lionel Robbins},
title = {An {E}ssay on the {N}ature \& {S}ignificance of {E}conomic {S}cience},
publisher = { Macmillan London },
year = {1932},
}

@book{kreps1990course,
  title={A Course in Microeconomic Theory},
  author={Kreps, D.M.},
  isbn={0691042640},
  lccn={8927619},
  url={https://books.google.at/books?id=nN1bPwAACAAJ},
  year={1990},
  publisher={Princeton University Press}
}


@book{katzner:walras,
  Author =       {Donald W. Katzner},
  Title =        {An Introduction to the Economic Theory of Market
                  Behavior: Microeconomics from a Walrasian
                  Perspective},
  Publisher =    {Edward Elgar Publishing Limited},
  Year =         {2006},
  ISBN =         {1845425103},
}

@book{arrow2010handbook,
  title={Handbook of Social Choice and Welfare},
  author={Arrow, Kenneth J and Sen, Amartya and Suzumura, Kotaro},
  volume={2},
  isbn = {978-0-444-50894-2},
  year={2010},
  publisher={Elsevier}
}

@inproceedings{DBLP:conf/cade/EchenimP17,
  author    = {Mnacho Echenim and
               Nicolas Peltier},
  title     = {The Binomial Pricing Model in Finance: {A} Formalization in Isabelle},
  booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on
               Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
  pages     = {546--562},
  year      = {2017},
  crossref  = {DBLP:conf/cade/2017},
  url       = {https://doi.org/10.1007/978-3-319-63046-5_33},
  doi       = {10.1007/978-3-319-63046-5_33},
  timestamp = {Wed, 12 Jul 2017 10:22:36 +0200},
  biburl    = {http://dblp.dagstuhl.de/rec/bib/conf/cade/EchenimP17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/cade/2017,
  editor    = {Leonardo de Moura},
  title     = {Automated Deduction - {CADE} 26 - 26th International Conference on
               Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10395},
  publisher = {Springer},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-63046-5},
  doi       = {10.1007/978-3-319-63046-5},
  isbn      = {978-3-319-63045-8},
  timestamp = {Wed, 12 Jul 2017 10:06:41 +0200},
  biburl    = {http://dblp.dagstuhl.de/rec/bib/conf/cade/2017},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}





@Article{MacKenzie2015,
author="MacKenzie, Simon
and Kerber, Manfred
and Rowat, Colin",
title={Pillage games with multiple stable sets},
journal="International Journal of Game Theory",
year="2015",
volume="44",
number="4",
pages="993--1013",
abstract="We prove that pillage games (Jordan in J Econ Theory 131.1:26--44, 2006, ``Pillage and property'', JET) can have multiple stable sets, constructing pillage games with up to                                                                           {\$}{\$}2^{\{}{\backslash}tfrac{\{}n-1{\}}{\{}3{\}}{\}}{\$}{\$}                                                                                    2                                                                                                            n                              -                              1                                                        3                                                                                                                               stable sets, when the number of agents,                                                                           {\$}{\$}n{\$}{\$}                                                            n                                                      , exceeds four. We do so by violating the anonymity axiom common to the existing literature to establish a power dichotomy: for all but a small exceptional set of endowments, powerful agents can overcome all the others; within the exceptional set, the lesser agents can defend their resources. Once the allocations giving powerful agents all resources are included in a candidate stable set, deriving the rest proceeds by considering dominance relations over the finite exceptional sets---reminiscent of stable sets' derivation in classical cooperative game theory. We also construct a multi-good pillage game with only three agents that also has two stable sets.",
issn="1432-1270",
doi="10.1007/s00182-015-0462-1",
url="https://doi.org/10.1007/s00182-015-0462-1"
}

@Article{Wiedijk2009,
author="Wiedijk, Freek",
title={{F}ormalizing {A}rrow's theorem},
journal="Sadhana",
year="2009",
volume="34",
number="1",
pages="193--220",
abstract="A small project in which I encoded a proof of Arrow's theorem---probably the most famous results in the economics field of social choice theory---in the computer using the Mizar system is presented here. The details of this specific project, as well as the process of formalization (encoding proofs in the computer) in general are discussed.",
issn="0973-7677",
doi="10.1007/s12046-009-0005-1",
url="https://doi.org/10.1007/s12046-009-0005-1"
}

@book{katzner2006introduction,
  title =        {An Introduction to the Economic Theory of Market
                  Behavior: Microeconomics from a Walrasian
                  Perspective},
  author =       {Katzner, Donald W.},
  isbn =         {1845425103},
  isbn13 = {9781845425104},
  year =         {2006},
  publisher =    {Edward Elgar Publishing Limited}
}

@inproceedings{DBLP:conf/tacas/FontaineMMNT06,
  author    = {Pascal Fontaine and
               Jean{-}Yves Marion and
               Stephan Merz and
               Leonor Prensa Nieto and
               Alwen Fernanto Tiu},
  title     = {{E}xpressiveness + {A}utomation + {S}oundness: {T}owards {C}ombining {SMT} {S}olvers
               and Interactive Proof Assistants},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
               12th International Conference, {TACAS} 2006 Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2006,
               Vienna, Austria, March 25 - April 2, 2006, Proceedings},
  pages     = {167--181},
  year      = {2006},
  crossref  = {DBLP:conf/tacas/2006},
  url       = {https://doi.org/10.1007/11691372_11},
  doi       = {10.1007/11691372_11},
  timestamp = {Thu, 28 May 2015 17:23:18 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tacas/FontaineMMNT06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/tacas/2006,
  editor    = {Holger Hermanns and
               Jens Palsberg},
  title     = {Tools and Algorithms for the Construction and Analysis of Systems,
               12th International Conference, {TACAS} 2006 Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2006,
               Vienna, Austria, March 25 - April 2, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3920},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11691372},
  doi       = {10.1007/11691372},
  isbn      = {3-540-33056-9},
  timestamp = {Thu, 28 May 2015 17:23:18 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tacas/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/tphol/PaulsonS07,
  author    = {Lawrence C. Paulson and
               Kong Woei Susanto},
  title     = {Source-Level Proof Reconstruction for Interactive Theorem Proving},
  booktitle = {Theorem Proving in Higher Order Logics, 20th International Conference,
               TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings},
  pages     = {232--245},
  year      = {2007},
  crossref  = {DBLP:conf/tphol/2007},
  url       = {https://doi.org/10.1007/978-3-540-74591-4_18},
  doi       = {10.1007/978-3-540-74591-4_18},
  timestamp = {Tue, 23 May 2017 01:12:08 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tphol/PaulsonS07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/tphol/2007,
  editor    = {Klaus Schneider and
               Jens Brandt},
  title     = {Theorem Proving in Higher Order Logics, 20th International Conference,
               TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4732},
  publisher = {Springer},
  year      = {2007},
  isbn      = {978-3-540-74590-7},
  timestamp = {Mon, 22 Dec 2014 14:25:11 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tphol/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/cade/BlanchetteBP11,
  author    = {Jasmin Christian Blanchette and
               Sascha B{\"{o}}hme and
               Lawrence C. Paulson},
  title     = {Extending Sledgehammer with {SMT} Solvers},
  booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on
               Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  pages     = {116--130},
  year      = {2011},
  crossref  = {DBLP:conf/cade/2011},
  url       = {https://doi.org/10.1007/978-3-642-22438-6_11},
  doi       = {10.1007/978-3-642-22438-6_11},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cade/BlanchetteBP11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/cade/2011,
  editor    = {Nikolaj Bj{\o}rner and
               Viorica Sofronie{-}Stokkermans},
  title     = {Automated Deduction - {CADE-23} - 23rd International Conference on
               Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6803},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-22438-6},
  doi       = {10.1007/978-3-642-22438-6},
  isbn      = {978-3-642-22437-9},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cade/2011},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@inproceedings{DBLP:conf/tphol/Roux09,
  author    = {St{\'{e}}phane Le Roux},
  title     = {{A}cyclic {P}references and {E}xistence of {S}equential {N}ash {E}quilibria: {A}
               Formal and Constructive Equivalence},
  booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
               TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
  pages     = {293--309},
  year      = {2009},
  crossref  = {DBLP:conf/tphol/2009},
  url       = {https://doi.org/10.1007/978-3-642-03359-9_21},
  doi       = {10.1007/978-3-642-03359-9_21},
  timestamp = {Tue, 17 Mar 2015 07:36:49 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tphol/Roux09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/tphol/2009,
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  title     = {Theorem Proving in Higher Order Logics, 22nd International Conference,
               TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5674},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-03359-9},
  doi       = {10.1007/978-3-642-03359-9},
  isbn      = {978-3-642-03358-2},
  timestamp = {Thu, 03 Sep 2009 22:10:29 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tphol/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}



@article{10.2307/1907353,
 ISSN = {00129682, 14680262},
 URL = {http://www.jstor.org/stable/1907353},
 abstract = {A. Wald has presented a model of production and a model of exchange and proofs of the existence of an equilibrium for each of them. Here proofs of the existence of an equilibrium are given for an integrated model of production, exchange and consumption. In addition the assumptions made on the technologies of producers and the tastes of consumers are significantly weaker than Wald's. Finally a simplification of the structure of the proofs has been made possible through use of the concept of an abstract economy, a generalization of that of a game.},
 author = {Kenneth J. Arrow and Gerard Debreu},
 journal = {Econometrica},
 number = {3},
 pages = {265-290},
 publisher = {[Wiley, Econometric Society]},
 title = {Existence of an Equilibrium for a Competitive Economy},
 volume = {22},
 year = {1954}
}

@book{tadelis2013game,
  title={Game Theory: An Introduction},
  author={Tadelis, Steven},
  isbn={9780691129082},
  year={2013},
  publisher={Princeton University Press}
}

@article{PeterJaeger2012,
abstract = {This article gives an elementary introduction to stochastic finance (in discrete time). A formalization of random variables is given and some elements of Borel sets are considered. Furthermore, special functions (for buying a present portfolio and the value of a portfolio in the future) and some statements about the relation between these functions are introduced. For details see: [8] (p. 185), [7] (pp. 12, 20), [6] (pp. 3-6).},
author = {Peter Jaeger},
journal = {Formalized Mathematics},
language = {eng},
number = {1},
pages = {1-5},
title = {Elementary Introduction to Stochastic Finance in Discrete Time},
url = {http://eudml.org/doc/267949},
volume = {20},
year = {2012},
}

@BOOK{RePEc:oxp:obooks:9780195102680,
title = {Microeconomic Theory},
author = {Mas-Colell, Andreu and Whinston, Michael and Green, Jerry},
year = {1995},
publisher = {Oxford University Press},
abstract = {This textbook aims to provide a comprehensive overview of the essentials of microeconomics. It offers unprecedented depth of coverage, whilst allowing lecturers to 'tailor-make' their courses to suit personal priorities. Covering topics such as noncooperative game theory, information economics, mechanism design and general equilibrium under uncertainty, it is written in a clear, accessible and engaging style and provides practice exercises and a full appendix of terminology.},
url = {http://EconPapers.repec.org/RePEc:oxp:obooks:9780195102680}
}

@article{pollack1998believe,
  title={How to believe a machine-checked proof},
  author={Pollack, Robert},
  journal={Twenty Five Years of Constructive Type Theory},
  volume={36},
  pages={205},
  year={1998},
  publisher={Clarendon Press}
}

@book{Nipkow:2014:CSI:2717090,
 author = {Nipkow, Tobias and Klein, Gerwin},
 title = {Concrete Semantics: With Isabelle/HOL},
 year = {2014},
 isbn = {3319105418, 9783319105413},
 publisher = {Springer Publishing Company, Incorporated},
}

@misc{progprove,
  title={Programming and {P}roving in {Isabelle/HOL}},
  author={Tobias Nipkow},
  year={2016},
  month = {December},
  url={https://isabelle.in.tum.de/doc/prog-prove.pdf}
}

@misc{wenzel2004isabelle,
  title={The {I}sabelle/{I}sar {R}eference {M}anual},
  author={Wenzel, Makarius and others},
  year={2016},
  url={https://isabelle.in.tum.de/doc/isar-ref.pdf}
}


@article{DBLP:journals:corr:CaminatiK0R13,
  author    = {Marco B. Caminati and
               Manfred Kerber and
               Christoph Lange and
               Colin Rowat},
  title     = {Proving soundness of combinatorial {V}ickrey auctions and generating
               verified executable code},
  journal   = {CoRR},
  volume    = {abs/1308.1779},
  year      = {2013},
  url       = {http://arxiv.org/abs/1308.1779},
  timestamp = {Tue, 10 Dec 2013 12:03:02 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/CaminatiK0R13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@incollection{inc:bruijn80a,
    address = {New York},
    author = {De Bruijn, N. G.},
    booktitle = {To H.\~{}B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
    citeulike-article-id = {428126},
    editor = {Seldin, J. P. and Hindley, J. R.},
    keywords = {automath, bibtex-import-all},
    pages = {579--606},
    posted-at = {2005-12-07 10:42:08},
    priority = {2},
    publisher = {Academic Press},
    title = {A Survey of the Project {AUTOMATH}},
    year = {1980}
}


@article{GomezBaggethun20101209,
title = {The history of ecosystem services in economic theory and practice: From early notions to markets and payment schemes},
journal = "Ecological Economics ",
volume = "69",
number = "6",
pages = "1209 - 1218",
year = "2010",
note = "Special Section - Payments for Environmental Services: Reconciling Theory and Practice ",
issn = "0921-8009",
doi = "https://doi.org/10.1016/j.ecolecon.2009.11.007",
url = "http://www.sciencedirect.com/science/article/pii/S092180090900456X",
author = "Erik Gómez-Baggethun and Rudolf de Groot and Pedro L. Lomas and Carlos Montes",
keywords = "Economic history",
keywords = "Use value",
keywords = "Exchange value",
keywords = "Ecosystem services",
keywords = "Market based instruments",
keywords = "Commodification ",
abstract = "This paper reviews the historic development of the conceptualization of ecosystem services and examines critical landmarks in economic theory and practice with regard to the incorporation of ecosystem services into markets and payment schemes. The review presented here suggests that the trend towards monetization and commodification of ecosystem services is partly the result of a slow move from the original economic conception of nature's benefits as use values in Classical economics to their conceptualization in terms of exchange values in Neoclassical economics. The theory and practice of current ecosystem services science are examined in the light of this historical development. From this review, we conclude that the focus on monetary valuation and payment schemes has contributed to attract political support for conservation, but also to commodify a growing number of ecosystem services and to reproduce the Neoclassical economics paradigm and the market logic to tackle environmental problems. "
}

@article{DBLP:journals:corr:HeuleKM16,
  author    = {Marijn J. H. Heule and
               Oliver Kullmann and
               Victor W. Marek},
  title     = {Solving and Verifying the boolean Pythagorean Triples problem via
               Cube-and-Conquer},
  journal   = {CoRR},
  volume    = {abs/1605.00723},
  year      = {2016},
  url       = {http://arxiv.org/abs/1605.00723},
  timestamp = {Wed, 01 Jun 2016 15:51:09 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/HeuleKM16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{kerber2013developing,
  title={Developing an Auction Theory Toolbox},
  author={Kerber, Manfred and Lange, Christoph and Rowat, Colin and Windsteiger, Wolfgang},
  journal={AISB 2013},
  pages={1--4},
  year={2013},
  publisher={Citeseer}
}

@inproceedings{paulson1990isabelle,
  title={Isabelle: The next 700 theorem provers},
  author={Paulson, Lawrence C},
  booktitle={Logic and computer science},
  volume={31},
  pages={361--386},
  year={1990}
}

@article{abc:conj:progres,
  author={Castelvecchi, Davide},
  month={July},
  year={2016},
  day={28},
  title={Monumental proof to torment mathematicians for years to come},
  number={7614},
  journal={Nature, International weekly journal of science},
  url={http://www.nature.com/news/monumental-proof-to-torment-mathematicians-for-years-to-come-1.20342},
  urldate={10-5-2016}
}

@article{DBLP:journals/afp/Nipkow08b,
  author    = {Tobias Nipkow},
  title     = {{A}rrow and {G}ibbard-{S}atterthwaite},
  journal   = {Archive of Formal Proofs},
  year      = {2008},
  url       = {https://www.isa-afp.org/entries/ArrowImpossibilityGS.shtml},
  timestamp = {Mon, 19 Sep 2016 15:58:56 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/afp/Nipkow08b},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}



@inproceedings{DBLP:conf/mkm/0002RK13,
  author    = {Christoph Lange and
               Colin Rowat and
               Manfred Kerber},
  title     = {The {F}or{M}a{R}{E} {P}roject - {F}ormal {M}athematical {R}easoning in {E}conomics},
  booktitle = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems
               and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12,
               2013. Proceedings},
  pages     = {330--334},
  year      = {2013},
  crossref  = {DBLP:conf/mkm/2013},
  url       = {https://doi.org/10.1007/978-3-642-39320-4_23},
  doi       = {10.1007/978-3-642-39320-4_23},
  timestamp = {Wed, 17 May 2017 10:54:57 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/mkm/0002RK13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/mkm/2013,
  editor    = {Jacques Carette and
               David Aspinall and
               Christoph Lange and
               Petr Sojka and
               Wolfgang Windsteiger},
  title     = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems
               and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12,
               2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7961},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-39320-4},
  doi       = {10.1007/978-3-642-39320-4},
  isbn      = {978-3-642-39319-8},
  timestamp = {Wed, 17 May 2017 10:54:57 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/mkm/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@article{tan2008first,
  title={The First Fundamental Theorem of Welfare Economics},
  author={Tan, Kegon Teng Kok},
  journal={Unpublished},
  year={2008}
}

@inproceedings{DBLP:conf/mkm/CaminatiK0R14,
  author    = {Marco B. Caminati and
               Manfred Kerber and
               Christoph Lange and
               Colin Rowat},
  title     = {Set Theory or Higher Order Logic to Represent Auction Concepts in
               Isabelle?},
  booktitle = {Intelligent Computer Mathematics - International Conference, {CICM}
               2014, Coimbra, Portugal, July 7-11, 2014. Proceedings},
  pages     = {236--251},
  year      = {2014},
  crossref  = {DBLP:conf/mkm/2014},
  url       = {https://doi.org/10.1007/978-3-319-08434-3_18},
  doi       = {10.1007/978-3-319-08434-3_18},
  timestamp = {Wed, 17 May 2017 10:54:57 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/mkm/CaminatiK0R14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/mkm/2014,
  editor    = {Stephen M. Watt and
               James H. Davenport and
               Alan P. Sexton and
               Petr Sojka and
               Josef Urban},
  title     = {Intelligent Computer Mathematics - International Conference, {CICM}
               2014, Coimbra, Portugal, July 7-11, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8543},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-08434-3},
  doi       = {10.1007/978-3-319-08434-3},
  isbn      = {978-3-319-08433-6},
  timestamp = {Wed, 17 May 2017 10:54:57 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/mkm/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{Rothe:2015:ECI:2829366,
author = {Rothe, Jrg},
title = {Economics and Computation: An Introduction to Algorithmic Game Theory, Computational Social Choice, and Fair Division},
year = {2015},
isbn = {3662479036, 9783662479032},
edition = {1st},
publisher = {Springer Publishing Company, Incorporated}
}

@misc{yanellis2003lecture,
  title={lecture Notes in General Equilibrium Theory},
  author={Yanellis, NC},
  year={2003},
  publisher={Dept. of Economics, University of Illinois at Urbana-Champaign}
}

@article{levin2006general,
  title={General equilibrium},
  author={Levin, Jonathan},
  journal={Harvard University},
  year={2006}
}

@electronic{kcborder:lec:demand0,
title={Technical Results on Regular Preferences and Demand},
author={K.C. Border},
year={2017},
url="http://people.hss.caltech.edu/~kcb/Notes/Demand0-Preferences.pdf",
urldate = {15.04.2017}
}

@Article{Paulson1989,
author="Paulson, Lawrence C.",
title={The foundation of a generic theorem prover},
journal="Journal of Automated Reasoning",
year="1989",
volume="5",
number="3",
pages="363--397",
abstract="Isabelle [28, 30] is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or `logical framework') in which the object-logics are formalized. Isabelle is now based on higher-order logic-a precise and well-understood foundation.",
issn="1573-0670",
doi="10.1007/BF00248324",
url="https://doi.org/10.1007/BF00248324"
}


@book{RePEc:pup:pbooks:9890,
title = {Microeconomic Foundations I: Choice and Competitive Markets},
author = {Kreps, David},
year = {2012},
edition = {1},
publisher = {Princeton University Press},
isbn={978-0691155838},
abstract = {Microeconomic Foundations I develops the choice, price, and general equilibrium theory topics typically found in first-year theory sequences, but in deeper and more complete mathematical form than most standard texts provide. The objective is to take the reader from acquaintance with these foundational topics to something closer to mastery of the models and results connected to them.},
keywords = {microeconomics; choice; price; equilibrium; economic models; preference; utility; consumer; demand; Afriat; Afriat's Theorem; uncertainty; dynamic choice; social choice; efficiency; competitive; profit-maximizing; expenditure; demand theory; deman; duality methods; surplus; aggregation; CET; dynamic programming}
}

@article{church_1940,
title={A formulation of the simple theory of types},
volume={5},
DOI={10.2307/2266170},
number={2},
journal={Journal of Symbolic Logic},
publisher={Cambridge University Press},
author={Church, Alonzo},
year={1940},
pages={56--68}
}

@book{advancedMicroTheory:Jehle:Reny,
title = {Advanced Microeconomic Theory},
author = {Geoffrey A. Jehle, Philip J. Reny},
year = {2011},
month = {April},
edition = {3},
publisher = {Pearson Education Limited},
isbn={0273731912 , 978-978-0273731917}
}

@article{hales2008formal,
  title={Formal proof},
  author={Hales, Thomas C},
  journal={Notices of the AMS},
  volume={55},
  number={11},
  pages={1370--1380},
  year={2008}
}

@article{SenSocialChoice-AFP,
  author  = {Peter Gammie},
  title   = {Some classical results in Social Choice Theory},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = {2008},
  note    = {\url{http://isa-afp.org/entries/SenSocialChoice.shtml},
            Formal proof development},
  ISSN    = {2150-914x}
}

@article{Randomised_Social_Choice-AFP,
  author  = {Manuel Eberl},
  title   = {Randomised Social Choice Theory},
  journal = {Archive of Formal Proofs},
  month   = may,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Randomised_Social_Choice.shtml},
            Formal proof development},
  ISSN    = {2150-914x}
}

@Inbook{Priestley2002,
author="Priestley, Hilary A.",
editor="Backhouse, Roland
and Crole, Roy
and Gibbons, Jeremy",
title={Ordered Sets and Complete Lattices},
bookTitle="Algebraic and Coalgebraic Methods in the Mathematics of Program Construction: International Summer School and Workshop Oxford, UK, April 10--14, 2000 Revised Lectures",
year="2002",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="21--78",
isbn="978-3-540-47797-6",
doi="10.1007/3-540-47797-7_2",
url="https://doi.org/10.1007/3-540-47797-7_2"
}


@inproceedings{DBLP:conf/cade/Harrison06,
  author    = {John Harrison},
  title     = {Towards Self-verification of {HOL} {L}ight},
  booktitle = {Automated Reasoning, Third International Joint Conference, {IJCAR}
               2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  pages     = {177--191},
  year      = {2006},
  crossref  = {DBLP:conf/cade/2006},
  url       = {https://doi.org/10.1007/11814771_17},
  doi       = {10.1007/11814771_17},
  timestamp = {Sun, 21 May 2017 00:17:17 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cade/Harrison06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@proceedings{DBLP:conf/cade/2006,
  editor    = {Ulrich Furbach and
               Natarajan Shankar},
  title     = {Automated Reasoning, Third International Joint Conference, {IJCAR}
               2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4130},
  publisher = {Springer},
  year      = {2006},
  isbn      = {3-540-37187-7},
  timestamp = {Wed, 22 Nov 2006 14:52:15 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cade/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@incollection{DBLP:series/hhl/HarrisonUW14,
  author    = {John Harrison and
               Josef Urban and
               Freek Wiedijk},
  title     = {History of Interactive Theorem Proving},
  booktitle = {Computational Logic},
  pages     = {135--214},
  year      = {2014},
  crossref  = {DBLP:series/hhl/9},
  url       = {https://doi.org/10.1016/B978-0-444-51624-4.50004-6},
  doi       = {10.1016/B978-0-444-51624-4.50004-6},
  timestamp = {Tue, 16 May 2017 14:24:38 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/series/hhl/HarrisonUW14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{DBLP:series/hhl/9,
  editor    = {J{\"{o}}rg H. Siekmann},
  title     = {Computational Logic},
  series    = {Handbook of the History of Logic},
  volume    = {9},
  publisher = {Elsevier},
  year      = {2014},
  isbn      = {978-0-444-51624-4},
  timestamp = {Mon, 03 Apr 2017 09:18:52 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/series/hhl/9},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{Tarski1936-TARDWI,
	volume = {1},
	title = {Der Wahrheitsbegriff in den {Formalisierten} {Sprachen}},
	pages = {261--405},
	journal = {Studia Philosophica},
	author = {Alfred Tarski},
	year = {1936}
}


@article{murawski:tarski:v:godel,
author = { Roman   Murawski },
title = {{U}ndefinability of {T}ruth. the {P}roblem of {p}riority:{T}arski vs {G}ödel},
journal = {History and Philosophy of Logic},
volume = {19},
number = {3},
pages = {153-160},
year = {1998},
doi = {10.1080/01445349808837306},
URL = {http://www.tandfonline.com/doi/abs/10.1080/01445349808837306},
eprint = { http://www.tandfonline.com/doi/pdf/10.1080/01445349808837306},
abstract = { The paper is devoted to the discussion of some philosophical and historical problems connected with the theorem on the undefinability of the notion of truth. In particular the problem of the priority of proving this theorem will be considered. It is claimed that Tarski obtained this theorem independently though he made clear his indebtedness to Gödel’s methods. On the other hand, Gödel was aware of the formal undefinability of truth in 1931, but he did not publish this result. Reasons for that are also considered }
}


@phdthesis{DBLP:phd/dnb/Wenzel02a,
  author    = {Markus Wenzel},
  title     = {Isabelle, Isar - a versatile environment for human readable formal
               proof documents},
  school    = {Technical University Munich, Germany},
  year      = {2002},
  url       = {http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.pdf},
  urn       = {urn:nbn:de:bvb:91-diss2002020117092},
  timestamp = {Fri, 20 Jan 2017 12:54:06 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/phd/dnb/Wenzel02a},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/types/HaftmannW06,
  author    = {Florian Haftmann and
               Makarius Wenzel},
  title     = {{C}onstructive {T}ype {C}lasses in {I}sabelle},
  booktitle = {Types for Proofs and Programs, International Workshop, {TYPES} 2006,
               Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
  pages     = {160--174},
  year      = {2006},
  crossref  = {DBLP:conf/types/2006},
  url       = {https://doi.org/10.1007/978-3-540-74464-1_11},
  doi       = {10.1007/978-3-540-74464-1_11},
  timestamp = {Sun, 21 May 2017 00:19:10 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/types/HaftmannW06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/types/2006,
  editor    = {Thorsten Altenkirch and
               Conor McBride},
  title     = {Types for Proofs and Programs, International Workshop, {TYPES} 2006,
               Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {4502},
  publisher = {Springer},
  year      = {2007},
  isbn      = {978-3-540-74463-4},
  timestamp = {Mon, 17 Sep 2007 12:52:22 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/types/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}



@Article{Paulson2004,
author="Paulson, Lawrence C.",
title={Organizing Numerical Theories Using Axiomatic Type Classes},
journal="Journal of Automated Reasoning",
year="2004",
volume="33",
number="1",
pages="29--49",
abstract="Mathematical reasoning may involve several arithmetic types, including those of the natural, integer, rational, real, and complex numbers. These types satisfy many of the same algebraic laws. These laws need to be made available to users, uniformly and preferably without repetition, but with due account for the peculiarities of each type. Subtyping, where a type inherits properties from a supertype, can eliminate repetition only for a fixed type hierarchy set up in advance by implementors. The approach recently adopted for Isabelle uses axiomatic type classes, an established approach to overloading. Abstractions such as semirings, rings, fields, and their ordered counterparts are defined, and theorems are proved algebraically. Types that meet the abstractions inherit the appropriate theorems.",
issn="1573-0670",
doi="10.1007/s10817-004-3997-6",
url="https://doi.org/10.1007/s10817-004-3997-6"
}


@article{Thompson:trustingTrust,
 author = {Thompson, Ken},
 title = {Reflections on Trusting Trust},
 journal = {Commun. ACM},
 issue_date = {Aug 1984},
 volume = {27},
 number = {8},
 month = aug,
 year = {1984},
 issn = {0001-0782},
 pages = {761--763},
 numpages = {3},
 url = {http://doi.acm.org/10.1145/358198.358210},
 doi = {10.1145/358198.358210},
 acmid = {358210},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@ARTICLE{wang60,
author={H. Wang},
journal={IBM Journal of Research and Development},
title={Toward Mechanical Mathematics},
year={1960},
volume={4},
number={1},
pages={2-22},
doi={10.1147/rd.41.0002},
ISSN={0018-8646},
month={Jan},
}

@article{Guard:1969:SM:321495.321500,
 author = {Guard, J. R. and Oglesby, F. C. and Bennett, J. H. and Settle, L. G.},
 title = {Semi-Automated Mathematics},
 journal = {J. ACM},
 issue_date = {Jan. 1969},
 volume = {16},
 number = {1},
 month = jan,
 year = {1969},
 issn = {0004-5411},
 pages = {49--62},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/321495.321500},
 doi = {10.1145/321495.321500},
 acmid = {321500},
 publisher = {ACM},
 address = {New York, NY, USA},
}
