Mon 8 Jan 2018 15:00 - 15:30 at Museum A - Verified Applications Chair(s): K. Rustan M. Leino

Economic activity has always been a fundamental part of society. With recent social and political changes economics has gained even more influence on our lives. In this paper we formalize two economic models in Isabelle/HOL: the pure exchange economy, where the only economic actors are consumers, as well as a version of the Arrow-Debreu Model, a private ownership economy, which includes production facilities. Interestingly, the definitions of various components of the economic models differ in the economic literature. We therefore show the equivalences and implications between various presentations, which allows us to create an extensible foundation for formalizing microeconomics and game theory compatible with multiple economic theories. We prove the First Theorem of Welfare Economics in both economic models. The theorem is the mathematical formulation of Adam Smith’s famous invisible hand and states that a group of self-interested and rational actors will eventually achieve an efficient allocation of goods. The formal proofs allow us to find more precise assumptions than those found in the economic literature.

Mon 8 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

13:30 - 15:30: CPP 2018 - Verified Applications at Museum A
Chair(s): K. Rustan M. LeinoAmazon
CPP-201813:30 - 14:00
Conrad WattUniversity of Cambridge, UK
CPP-201814:00 - 14:30
Sidney AmaniUNSW, Australia, Myriam BégelENS Paris-Saclay, France, Maksym Bortin, Mark StaplesCSIRO, Australia
CPP-201814:30 - 15:00
George PîrleaUniversity College London, Ilya SergeyUniversity College London
DOI Pre-print
CPP-201815:00 - 15:30
Cezary KaliszykUniversity of Innsbruck, Julian ParsertUniversity of Innsbruck, Austria