@book{smith1776WealthOfNations,
  title={An {I}nquiry Into the {N}ature and {C}auses of the {W}ealth of {N}ations},
  author={Smith, Adam},
  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}
}

@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}
}

@article{nash1950equilibrium,
  title={Equilibrium points in n-person games},
  author={Nash, John F and others},
  journal={Proceedings of the national academy of sciences},
  volume={36},
  number={1},
  pages={48--49},
  year={1950},
  publisher={USA}
}

@article{LEROUX2018,
title = "Extending finite-memory determinacy to multi-player games",
journal = "Information and Computation",
year = "2018",
issn = "0890-5401",
doi = "https://doi.org/10.1016/j.ic.2018.02.024",
url = "http://www.sciencedirect.com/science/article/pii/S0890540118300270",
author = "Stéphane Le Roux and Arno Pauly",
keywords = "Finite memory, Games played on finite graphs, Finite-memory determinacy, Nash equilibrium, Equilibrium transfer, Energy parity games",
abstract = "We show that under some general conditions the finite memory determinacy of a class of two-player win/lose games played on finite graphs implies the existence of a Nash equilibrium built from finite memory strategies for the corresponding class of multi-player multi-outcome games. This generalizes a previous result by Brihaye, De Pril and Schewe. We provide a number of example that separate the various criteria we explore. Our proofs are generally constructive, that is, provide upper bounds for the memory required, as well as algorithms to compute the relevant Nash equilibria."
}

@InProceedings{ Ma2018.4,
author = {Martin-Dorel, Erik and Soloviev, Sergei},
title = "{A Formal Study of Boolean Games with Random Formulas as Payoff Functions (regular paper)}",
booktitle = "{Types, Novi Sad, 23/05/2016-26/05/2016}",
editor = {Geuvers, Herman and Ghilezan, Silvia and Ivetic, Jelena},
year = {2018},
to_appear = {to appear},
publisher = {Schloss Dagstuhl Leibniz-Zentrum fur Informatik},
address = {http://www.dagstuhl.de/en/publications/},
series = {LIPICS},
pages = {},
language = {anglais},
keywords = {Boolean Games, Random process, Coq formal proofs},
abstract = {A probabilistic analysis of Boolean games is presented. The class of Boolean games with payoff functions given by random Boolean formulas is studied. This permits to study certain properties of this class in its totality, such as the probability of the existence of a winning strategy, including its asymptotic behavior. With the help of the Coq proof assistant, we develop a Coq library of Boolean games, to provide a formal proof of our results, and a basis for future development.}
}

@article{JFR7235,
	author = {Alexander Bagnall and Samuel Merten and Gordon Stewart},
	title = {A Library for Algorithmic Game Theory in Ssreflect/Coq},
	journal = {Journal of Formalized Reasoning},
	volume = {10},
	number = {1},
	year = {2017},
	keywords = {Coq; Ssreflect; Algorithmic Game Theory},
	issn = {1972-5787},	pages = {67--95},	doi = {10.6092/issn.1972-5787/7235},
	url = {https://jfr.unibo.it/article/view/7235}
}

@article{DBLP:journals/ipl/Vestergaard06,
  author    = {Ren{\'{e}} Vestergaard},
  title     = {A constructive approach to sequential Nash equilibria},
  journal   = {Inf. Process. Lett.},
  volume    = {97},
  number    = {2},
  pages     = {46--51},
  year      = {2006},
  url       = {https://doi.org/10.1016/j.ipl.2005.09.010},
  doi       = {10.1016/j.ipl.2005.09.010},
  timestamp = {Fri, 26 May 2017 22:54:46 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/ipl/Vestergaard06},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1709-02096,
  author    = {St{\'{e}}phane Le Roux and
               {\'{E}}rik Martin{-}Dorel and
               Jan{-}Georg Smaus},
  title     = {An Existence Theorem of {N}ash {E}quilibrium in {C}oq and {I}sabelle},
  booktitle = {Proceedings Eighth International Symposium on Games, Automata, Logics
               and Formal Verification, GandALF 2017, Roma, Italy, 20-22 September
               2017.},
  pages     = {46--60},
  year      = {2017},
  crossref  = {DBLP:journals/corr/abs-1709-01761},
  url       = {https://doi.org/10.4204/EPTCS.256.4},
  doi       = {10.4204/EPTCS.256.4},
  timestamp = {Mon, 23 Oct 2017 07:04:16 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-02096},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:journals/corr/abs-1709-01761,
  editor    = {Patricia Bouyer and
               Andrea Orlandini and
               Pierluigi San Pietro},
  title     = {Proceedings Eighth International Symposium on Games, Automata, Logics
               and Formal Verification, GandALF 2017, Roma, Italy, 20-22 September
               2017},
  series    = {{EPTCS}},
  volume    = {256},
  year      = {2017},
  url       = {http://arxiv.org/abs/1709.01761},
  timestamp = {Mon, 16 Oct 2017 16:32:11 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-01761},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@book{kreps1988notes,
  title={Notes On The Theory Of Choice},
  author={Kreps, D.},
  isbn={9780813346465},
  lccn={88004975},
  series={Underground Classics in Economics},
  url={https://books.google.at/books?id=9D0Oljs5GrQC},
  year={1988},
  publisher={Avalon Publishing}
}

@InProceedings{passmoreInf,
author="Passmore, Grant Olney
and Ignatovich, Denis",
editor="de Moura, Leonardo",
title="Formal Verification of Financial Algorithms",
booktitle="Automated Deduction -- CADE 26",
year="2017",
publisher="Springer",
pages="26--41",
abstract="Many deep issues plaguing today's financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Aesthetic Integration, we have pioneered the use of formal verification for analysing the safety and fairness of financial algorithms. With a focus on financial infrastructure (e.g., the matching logics of exchanges and dark pools and FIX connectivity between trading systems), we describe the landscape, and illustrate our Imandra formal verification system on a number of real-world examples. We sketch many open problems and future directions along the way.",
isbn="978-3-319-63046-5"
}

@phdthesis{DBLP:phd/dnb/Holzl13,
  author    = {Johannes H{\"{o}}lzl},
  title     = {Construction and stochastic applications of measure spaces in higher-order
               logic},
  school    = {Technical University Munich},
  year      = {2013},
  url       = {http://nbn-resolving.de/urn:nbn:de:bvb:91-diss-20130219-1116512-0-6},
  urn       = {urn:nbn:de:bvb:91-diss-20130219-1116512-0-6},
  timestamp = {Tue, 19 Apr 2016 15:30:15 +0200},
  biburl    = {http://dblp.org/rec/bib/phd/dnb/Holzl13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

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

@article{10.2307/1914185,
 ISSN = {00129682, 14680262},
 URL = {http://www.jstor.org/stable/1914185},
 abstract = {This paper presents a critique of expected utility theory as a descriptive model of decision making under risk, and develops an alternative model, called prospect theory. Choices among risky prospects exhibit several pervasive effects that are inconsistent with the basic tenets of utility theory. In particular, people underweight outcomes that are merely probable in comparison with outcomes that are obtained with certainty. This tendency, called the certainty effect, contributes to risk aversion in choices involving sure gains and to risk seeking in choices involving sure losses. In addition, people generally discard components that are shared by all prospects under consideration. This tendency, called the isolation effect, leads to inconsistent preferences when the same choice is presented in different forms. An alternative theory of choice is developed, in which value is assigned to gains and losses rather than to final assets and in which probabilities are replaced by decision weights. The value function is normally concave for gains, commonly convex for losses, and is generally steeper for losses than for gains. Decision weights are generally lower than the corresponding probabilities, except in the range of low probabilities. Overweighting of low probabilities may contribute to the attractiveness of both insurance and gambling.},
 author = {Daniel Kahneman and Amos Tversky},
 journal = {Econometrica},
 number = {2},
 pages = {263-291},
 publisher = {[Wiley, Econometric Society]},
 title = {Prospect Theory: An Analysis of Decision under Risk},
 volume = {47},
 year = {1979}
}

@article {Tversky1124,
	author = {Tversky, Amos and Kahneman, Daniel},
	title = {Judgment under Uncertainty: Heuristics and Biases},
	volume = {185},
	number = {4157},
	pages = {1124--1131},
	year = {1974},
	doi = {10.1126/science.185.4157.1124},
	publisher = {American Association for the Advancement of Science},
	abstract = {This article described three heuristics that are employed in making judgements under uncertainty: (i) representativeness, which is usually employed when people are asked to judge the probability that an object or event A belongs to class or process B; (ii) availability of instances or scenarios, which is often employed when people are asked to assess the frequency of a class or the plausibility of a particular development; and (iii) adjustment from an anchor, which is usually employed in numerical prediction when a relevant value is available. These heuristics are highly economical and usually effective, but they lead to systematic and predictable errors. A better understanding of these heuristics and of the biases to which they lead could improve judgements and decisions in situations of uncertainty.},
	issn = {0036-8075},
	URL = {http://science.sciencemag.org/content/185/4157/1124},
	eprint = {http://science.sciencemag.org/content/185/4157/1124.full.pdf},
	journal = {Science}
}

@inproceedings{Parsert:2018:FMF:3176245.3167100,
 author = {Parsert, Julian and Kaliszyk, Cezary},
 title = {Formal {M}icroeconomic {F}oundations and the {F}irst {W}elfare {T}heorem},
 booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
 series = {CPP 2018},
 year = {2018},
 isbn = {978-1-4503-5586-5},
 location = {Los Angeles, CA, USA},
 pages = {91--101},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/3167100},
 doi = {10.1145/3167100},
 acmid = {3167100},
 publisher = {ACM},
 keywords = {First Welfare Theorem, Game Theory, Isabelle, Microeconomics},
} 


@techreport{NBERw3641,
  title =        "The Invisible Hand and Modern Welfare Economics",
  author =       "Joseph E. Stiglitz",
  institution =  "National Bureau of Economic Research",
  type =         "Working Paper",
  series =       "Working Paper Series",
  number =       "3641",
  year =         "1991",
  month =        "March",
  doi =          {10.3386/w3641},
  URL =          "http://www.nber.org/papers/w3641",
  abstract =     {This paper reviews and puts into perspective recent
                  work reassessing the first and second Fundamental
                  Theorems of Welfare Economics. It assesses the
                  implications of the Greenwald-Stiglitz theorem
                  establishing the (constrained) Pareto inefficiency
                  of market economies with imperfect information and
                  incomplete markets as well as recent work on
                  endogenous technological change. The information
                  theoretic limitations to the Second Fundamental
                  Theorem are also discussed, including the inability
                  to separate out issues of equity and efficiency. The
                  final sections of the paper consider the
                  consequences of these problems for economic
                  organization, economic policy, and the role of
                  ideology in the belief in the Invisible Hand.},
}

@article{BLUME20151,
title = "Introduction to computer science and economic theory",
journal = "Journal of Economic Theory",
volume = "156",
number = "Supplement C",
pages = "1 - 13",
year = "2015",
note = "Computer Science and Economic Theory",
issn = "0022-0531",
doi = "https://doi.org/10.1016/j.jet.2014.11.002",
url = "http://www.sciencedirect.com/science/article/pii/S0022053114001616",
author = "Lawrence Blume and David Easley and Jon Kleinberg and Robert Kleinberg and Éva Tardos",
keywords = "Algorithmic game theory",
keywords = "Implementation",
keywords = "Learning in games",
keywords = "Mechanism design",
keywords = "Networks",
abstract = "Abstract This essay introduces the symposium on computer science and economic theory."
}

@book{Nisan:2007:AGT:1296179,
  author =       {Nisan, Noam and Roughgarden, Tim and Tardos, Eva and
                  Vazirani, Vijay V.},
  title =        {Algorithmic Game Theory},
  year =         {2007},
  isbn =         {0521872820},
  publisher =    {Cambridge University Press},
  address =      {New York, NY, USA},
}

@Inbook{Haftmann2007,
author="Haftmann, Florian
and Wenzel, Makarius",
editor="Altenkirch, Thorsten
and McBride, Conor",
title="Constructive Type Classes in Isabelle",
bookTitle="Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers",
year="2007",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="160--174",
abstract="We reconsider the well-known concept of Haskell-style type classes within the logical framework of Isabelle. So far, axiomatic type classes in Isabelle merely account for the logical aspect as predicates over types, while the operational part is only a convention based on raw overloading. Our more elaborate approach to constructive type classes provides a seamless integration with Isabelle locales, which are able to manage both operations and logical properties uniformly. Thus we combine the convenience of type classes and the flexibility of locales. Furthermore, we construct dictionary terms derived from notions of the type system. This additional internal structure provides satisfactory foundations of type classes, and supports further applications, such as code generation and export of theories and theorems to environments without type classes.",
isbn="978-3-540-74464-1",
doi="10.1007/978-3-540-74464-1_11",
url="https://doi.org/10.1007/978-3-540-74464-1_11"
}



@article{10.1257/aer.97.1.242,
  Author =       {Edelman, Benjamin and Ostrovsky, Michael and
                  Schwarz, Michael},
  Title =        {Internet Advertising and the Generalized
                  Second-Price Auction: Selling Billions of Dollars
                  Worth of Keywords},
  Journal =      {American Economic Review},
  Volume =       {97},
  Number =       {1},
  Year =         {2007},
  Month =        {March},
  Pages =        {242-259},
  DOI =          {10.1257/aer.97.1.242},
  URL =
                  {http://www.aeaweb.org/articles?id=10.1257/aer.97.1.242}
}

@book{von1947theory,
  title={Theory of Games and Economic Behavior},
  author={Von Neumann, J. and Morgenstern, O.},
  lccn={a44004629},
  url={https://books.google.at/books?id=AUDPAAAAMAAJ},
  year={1947},
  publisher={Princeton University Press}
}

@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",
  abstract =     "Locales are a module system for managing theory
                  hierarchies in a theorem prover through theory
                  interpretation. They are available for the theorem
                  prover Isabelle. In this paper, their semantics is
                  defined in terms of local theories and morphisms.
                  Locales aim at providing flexible means of extension
                  and reuse. Theory modules (which are called locales)
                  may be extended by definitions and theorems.
                  Interpretation to Isabelle's global theories and
                  proof contexts is possible via morphisms. Even the
                  locale hierarchy may be changed if declared
                  relations between locales do not adequately reflect
                  logical relations, which are implied by the locales'
                  specifications. By discussing their design and
                  relating it to more commonly known structuring
                  mechanisms of programming languages and provers,
                  locales are made accessible to a wider audience
                  beyond the users of Isabelle. The discussed
                  mechanisms include ML-style functors, type classes
                  and mixins (the latter are found in modern
                  object-oriented languages).",
  issn =         "1573-0670",
  doi =          "10.1007/s10817-013-9284-7",
  url =          "https://doi.org/10.1007/s10817-013-9284-7"
}

@article{Randomised:Social:ChoiceAFP,
  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}
}

@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}
}

@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}
}


@article{doi:10.1093/cesifo/ifq017,
author = {Kirman, Alan},
title = {The Economic Crisis is a Crisis for Economic Theory*},
journal = {CESifo Economic Studies},
volume = {56},
number = {4},
pages = {498-535},
year = {2010},
doi = {10.1093/cesifo/ifq017},
URL = { + https://doi.org/10.1093/cesifo/ifq017},
}

@article{formula:crashed:market,
  author =       {Ian Stewart},
  title =        {The mathematical equation that caused the banks to
                  crash},
  journal =      {The Guardian},
  day =          12,
  month =        {February},
  year =         2012,
  note =
                  {www.theguardian.com/science/2012/feb/12/black-scholes-equation-credit-crunch
                  [Last accessed: 3rd October 2017]},
}

@article {JEEA:JEEA1030,
author = {Stiglitz, Joseph E.},
title = {Rethinking Macroeconomics: What failed, and how to repair it},
journal = {Journal of the European Economic Association},
volume = 9,
number = 4,
publisher = {Blackwell Publishing Inc},
issn = {1542-4774},
url = {https://doi.org/10.1111/j.1542-4774.2011.01030.x},
doi = {10.1111/j.1542-4774.2011.01030.x},
pages = {591--645},
year = 2011,
}

@Inbook{Geanakoplos1989,
author="Geanakoplos, John",
editor="Eatwell, John
and Milgate, Murray
and Newman, Peter",
title="Arrow-Debreu Model of General Equilibrium",
bookTitle="General Equilibrium",
year="1989",
publisher="Palgrave Macmillan UK",
address="London",
pages="43--61",
abstract="It is not easy to separate the significance and influence of the Arrow--Debreu model of general equilibrium from that of mathematical economics itself. In an extraordinary series of papers (Arrow, 1951 ; Debreu, 1951; Arrow--Debreu, 1954), two of the oldest and most important questions of neoclassical economics, the viability and efficiency of the market system, were shown to be susceptible to analysis in a model completely faithful to the neoclassical methodological premises of individual rationality, market clearing, and rational expectations, through arguments at least as elegant as any in economic theory, using the two techniques (convexity and fixed point theory) that are still, after thirty years, the most important mathematical devices in mathematical economics. Fifteen years after its birth (e.g. Arrow, 1969), the model was still being reinterpreted to yield fresh economic insights, and twenty years later the same model was still capable of yielding new and fundamental mathematical properties (e.g. Debreu, 1970, 1974). When we consider that the same two men who derived the most fundamental properties of the model (along with McKenzie, 1954) also provided the most significant economic interpretations, it is no wonder that its invention has helped earn for each of its creators, in different years, the Nobel Prize for economics.",
isbn="978-1-349-19802-3",
doi="10.1007/978-1-349-19802-3_3",
url="https://doi.org/10.1007/978-1-349-19802-3_3"
}

@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{DBLP:journals/tcs/Blanck00,
  author    = {Jens Blanck},
  title     = {Domain representations of topological spaces},
  journal   = {Theor. Comput. Sci.},
  volume    = {247},
  number    = {1-2},
  pages     = {229--255},
  year      = {2000},
  url       = {https://doi.org/10.1016/S0304-3975(99)00045-6},
  doi       = {10.1016/S0304-3975(99)00045-6},
  timestamp = {Sun, 28 May 2017 13:20:02 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tcs/Blanck00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

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

@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}
}

@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}
}



@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    = {LNCS},
  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}
}


@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 = {MKM, Calculemus, DML, and Systems
               and Projects 2013, Bath, UK, July 8-12,
               2013. Proceedings},
  pages     = {330--334},
  year      = {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     = {MKM, Calculemus, DML, Bath, UK, July 8-12,
               2013. Proceedings},
  series    = {LNCS},
  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{COX1979229,
  title =        "Option pricing: A simplified approach",
  journal =      "Journal of Financial Economics",
  volume =       "7",
  number =       "3",
  pages =        "229 - 263",
  year =         "1979",
  issn =         "0304-405X",
  doi =          "https://doi.org/10.1016/0304-405X(79)90015-1",
  url =
                  "http://www.sciencedirect.com/science/article/pii/0304405X79900151",
  author =       "John C. Cox and Stephen A. Ross and Mark Rubinstein",
  abstract =     "Abstract This paper presents a simple discrete-time
                  model for valuing options. The fundamental economic
                  principles of option pricing by arbitrage methods
                  are particularly clear in this setting. Its
                  development requires only elementary mathematics,
                  yet it contains as a special limiting case the
                  celebrated Black-Scholes model, which has previously
                  been derived only by much more difficult methods.
                  The basic model readily lends itself to
                  generalization in many ways. Moreover, by its very
                  construction, it gives rise to a simple and
                  efficient numerical procedure for valuing options
                  for which premature exercise may be optimal."
}


@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.uni-trier.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    = {LNCS},
  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.uni-trier.de/rec/bib/conf/cade/2017},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@Article{Wiedijk2009,
author="Wiedijk, Freek",
title="Formalizing {A}rrow's theorem",
journal="Sadhana",
year="2009",
month="Feb",
day="01",
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"
}

@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},
}

@article{StableMatching:AFP,
  author  = {Peter Gammie},
  title   = {Stable Matching},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Stable_Matching.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@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.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@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, David 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{micro:colell,
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{Nash50,
  volume = {36},
  title = {Equilibrium points in $n$-person games},
  author = {John F. Nash},
  pages = {48-49},
  year = {1950},
volume = {36},
    issn = {00278424},
    journal = {Proceedings of the National Academy of Sciences of the United States of America},
}

@book{maschler:solan:zamir:2013,
place={Cambridge}, 
title={Game Theory}, 
DOI={10.1017/CBO9780511794216}, 
publisher={Cambridge University Press}, 
author={Maschler, Michael and Solan, Eilon and Zamir, Shmuel}, 
year={2013},
isbn={9781107005488}
}

@Inbook{Caminati2014,
author="Caminati, Marco B.
and Kerber, Manfred
and Lange, Christoph
and Rowat, Colin",
editor="Watt, Stephen M.
and Davenport, James H.
and Sexton, Alan P.
and Sojka, Petr
and Urban, Josef",
title="Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?",
bookTitle="CICM 2014, Coimbra, Portugal, July 7-11, 2014.",
year="2014",
publisher="Springer",
pages="236--251",
abstract="When faced with the question of how to represent properties in a formal proof system any user has to make design decisions. We have proved three of the theorems from Maskin's 2004 survey article on Auction Theory using the Isabelle/HOL system, and we have verified software code that implements combinatorial Vickrey auctions. A fundamental question in this was how to represent some basic concepts: since set theory is available inside Isabelle/HOL, when introducing new definitions there is often the issue of balancing the amount of set-theoretical objects and of objects expressed using entities which are more typical of higher order logic such as functions or lists. Likewise, a user has often to answer the question whether to use a constructive or a non-constructive definition. Such decisions have consequences for the proof development and the usability of the formalization. For instance, sets are usually closer to the representation that economists would use and recognize, while the other objects are closer to the extraction of computational content. We have studied the advantages and disadvantages of these approaches, and their relationship, in the concrete application setting of auction theory. In addition, we present the corresponding Isabelle library of definitions and theorems, most prominently those dealing with relations and quotients.",
isbn="978-3-319-08434-3",
doi="10.1007/978-3-319-08434-3_18",
url="https://doi.org/10.1007/978-3-319-08434-3_18"
}

@article{DBLP:journals/afp/ParsertK17,
  author    = {Julian Parsert and
               Cezary Kaliszyk},
  title     = {{M}icroeconomics and the {F}irst {W}elfare {T}heorem},
  journal   = {Archive of Formal Proofs},
  volume    = {2017},
  year      = {2017},
  url       = {https://www.isa-afp.org/entries/First_Welfare_Theorem.html},
  timestamp = {Tue, 19 Sep 2017 15:50:24 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/afp/ParsertK17},
  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 = {Wed, 12 Jul 2017 15:13:23 +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}
}

@inproceedings{isabelle,
  author    = {Makarius Wenzel and
               Lawrence C. Paulson and
               Tobias Nipkow},
  title     = {The {I}sabelle Framework},
  booktitle = {Theorem Proving in Higher Order Logics, 21st International Conference,
               TPHOLs 2008},
  pages     = {33--38},
  year      = {2008},
  editor    = {Otmane A{\"{\i}}t Mohamed and
               C{\'{e}}sar A. Mu{\~{n}}oz and
               Sofi{\`{e}}ne Tahar},
  series    = {LNCS},
  volume    = {5170},
  publisher = {Springer},
  doi       = {10.1007/978-3-540-71067-7_7},
}

@MISC{Wenzel11isarref,
    author = {Makarius Wenzel},
    title = {The {I}sabelle/{I}sar {R}eference {M}anual},
    year = {2017}
}