Advertisement

Dependently-Typed Programming in Scientific Computing

Examples from Economic Modelling
  • Cezar IonescuEmail author
  • Patrik Jansson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8241)

Abstract

Computer simulations are essential in virtually every scientific discipline, even more so in those such as economics or climate change where the ability to make laboratory experiments is limited. Therefore, it is important to ensure that the models are implemented correctly, that they can be re-implemented and that the results can be reproduced. Typically, though, the models are described by a mixture of prose and mathematics which is insufficient for these purposes. We argue that using dependent types allows us to gradually reduce the gap between the mathematical description and the implementation, and we give examples from economic modelling. We discuss the consequences that our incremental approach has on programming style and the requirements it imposes on the dependently-typed programming languages used.

Keywords

Equilibrium Price Type Theory Scientific Computing Initial Endowment Computable General Equilibrium Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
  2. 2.
  3. 3.
    GEM-E3 Website. http://www.gem-e3.net/
  4. 4.
  5. 5.
    Bellman, R.E.: Dynamic Programming. Princeton University Press, Princeton (1957)zbMATHGoogle Scholar
  6. 6.
    Bertsekas, D.P.: Dynamic Programming and Optimal Control, 2nd edn. Athena Scientific, Belmont (2000)Google Scholar
  7. 7.
    Brady, E., Hammond, K.: Correct-by-construction concurrency: using dependent types to verify implementations of effectful resource usage protocol. Fundamenta Informaticae 102, 145–176 (2010)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Dijkstra, E.W.: A constructive approach to the problem of program correctness. BIT Numer. Math. 8(3), 174–186 (1968)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Evensen, P., Märdin, M.: An extensible and scalable agent-based simulation of barter economics. Master’s thesis 2009/04a, Chalmers University of Technology and University of Gothenburg (2009)Google Scholar
  10. 10.
    Gintis, H.: The emergence of a price system from decentralized bilateral exchange. B.E. J. Theor. Econ. 6(1), 13 (2006)MathSciNetGoogle Scholar
  11. 11.
    Kreinovich, V.: Designing, understanding, and analyzing unconventional computation: the important role of logic and constructive mathematics. Appl. Math. Sci. 6(13–16), 645–649 (2012)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Martin-Löf, P.: Constructive mathematics and computer programming. Philos. Trans. R. Soc. Lond. 312(1522), 501–518 (1984)CrossRefzbMATHGoogle Scholar
  13. 13.
  14. 14.
    Mu, S.-C., Ko, H.-S., Jansson, P.: Algebra of programming in Agda: dependent types for relational program derivation. J. Funct. Program. 19, 545–579 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf’s Type Theory. Oxford University Press, Oxford (1990)zbMATHGoogle Scholar
  16. 16.
    Nordström, B., Petersson, K., Smith, J.: Martin-Löf type theory. In: Handbook of Logic in Computer Science, vol. 5, pp. 1–37. Oxford University Press, Oxford (2000)Google Scholar
  17. 17.
    Nordström, B., Smith, J.: Propositions and specifications of programs in Martin-Löf’s type theory. BIT Numer. Math. 24, 288–301 (1984)CrossRefzbMATHGoogle Scholar
  18. 18.
    Suppes, P.: Introduction to Logic. Dover Books on Mathematics Series. Dover, New York (1999). (Reprint of the 1957 edition from Van Nostrand)Google Scholar
  19. 19.
    Swierstra, W.: A Hoare logic for the state monad. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 440–451. Springer, Heidelberg (2009)Google Scholar
  20. 20.
    Thompson, S.: Type Theory and Functional Programming. Addison-Wesley, Redwood (1991)zbMATHGoogle Scholar
  21. 21.
    Thompson, S.: Are subsets necessary in Martin-Löf type theory? In: Myers Jr, J.P., O’Donnell, M.J. (eds.) Constructivity in CS 1991. LNCS, vol. 613. Springer, Heidelberg (1992)Google Scholar
  22. 22.
    Turner, R.: Computable Models. Springer, London (2009)CrossRefzbMATHGoogle Scholar
  23. 23.
    Varian, H.R.: Microeconomic Analysis. Norton, New York (1992)Google Scholar
  24. 24.
    Velupillai, K.: Computable Economics: The Arne Ryde Memorial Lectures. Oxford University Press, Oxford (2000)CrossRefGoogle Scholar
  25. 25.
    Velupillai, K.V.: Algorithmic foundations of computable general equilibrium theory. Appl. Math. Comput. 179, 360–369 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Velupillai, K.V.: Taming the incomputable, reconstructing the nonconstructive and deciding the undecidable in mathematical economics. New Math. Nat. Comput. (NMNC) 8(01), 5–51 (2012)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Walras, L.: Elements of Pure Economics: Or the Theory of Social Wealth. Routledge Library Editions-Economics. Taylor & Francis Group, London (1954)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  1. 1.Potsdam Institute for Climate Impact ResearchPotsdamGermany
  2. 2.Chalmers University of TechnologyGöteborgSweden

Personalised recommendations