ForMaRE – Formal Mathematical Reasoning in Economics
ForMaRE applies formal mathematical reasoning to economics.
We seek to increase confidence in economics' theoretical results, to aid in discovering new results, and to foster interest in formal methods, i.e. computer-aided reasoning, within economics.
To computer science, we seek to present user experience feedback from new audiences, as well as new challenge problems, thus contributing to the development of formal methods.
For more details, we recommend this short project description, as well as our publications.
Newssubscribe
- 2013-Aug-23: The source code of the Auction Theory Toolbox (ATT) is now hosted on Github to allow for easier participation in the development. (Read more)
- 2013-Jul-05: The date of our half-day tutorial on Applying Mechanised Reasoning in Economics – Making Reasoners Applicable for Domain Experts at Informatik 2013 in Koblenz, Germany, has been fixed to 17 September (afternoon). Early registration is possible until 15 July. (Read more)
- 2013-Jun-12: We invite high-quality original research papers to a special issue of Mathematics in Computer Science titled “Enabling Domain Experts to use Formalised Reasoning”. Submission deadline is 31 October. (Read more)
- Older news items are in the archive.
Public resources and outputs
- Auction Theory Toolbox (ATT), currently featuring formalisations in Isabelle/HOL and CASL
- project community site (powered by Planetary)
- Mailing lists: general discussion forum, announcements from the project members (e.g. about events, new formalisations, software releases)
Selected publicationsfull publication list
- Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat. Proving soundness of combinatorial Vickrey auctions and generating verified executable code. arXiv, 2013. (accompanying formalisations and implementations evolve in the Auction Theory Toolbox) First writeup on generating verified auction software
- Christoph Lange, Colin Rowat, Manfred Kerber. The ForMaRE Project – Formal Mathematical Reasoning in Economics. Conference on Intelligent Computer Mathematics (CICM, systems & projects track). No. 7961 in Lecture Notes in Computer Science, Springer, pp. 330–334, 2013. Project description and first-year summary, from a formal methods perspective
- Christoph Lange, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, Wolfgang Windsteiger. A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. Conference on Intelligent Computer Mathematics (CICM, mathematical knowledge management track). No. 7961 in Lecture Notes in Computer Science, Springer, pp. 200–215, 2013. (accompanying formalisations evolve in the Auction Theory Toolbox)
- Manfred Kerber, Christoph Lange, Colin Rowat. An economist's guide to mechanized reasoning or My computer just proved 84 impossibility theorems. Initiative for Computational Economics, 2012 (invited lecture). Overview on the potential of applying formal methods to economics, from an economics perspective
Peopledetails about the people behind ForMaRE
At the University of Birmingham, ForMaRE is run by Manfred Kerber, Colin Rowat, and Christoph Lange.
We collaborate with a number of external international researchers, including computer scientists as well as economists.
Funding
This research is funded by EPSRC grant EP/J007498/1 (“Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour”).
Internal
Internal information for the project members
This page was last modified on 23 August 2013.