{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,3]],"date-time":"2025-08-03T04:20:09Z","timestamp":1754194809949,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642415814"},{"type":"electronic","value":"9783642415821"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41582-1_9","type":"book-chapter","created":{"date-parts":[[2013,11,15]],"date-time":"2013-11-15T12:38:21Z","timestamp":1384519101000},"page":"140-156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Dependently-Typed Programming in Scientific Computing"],"prefix":"10.1007","author":[{"given":"Cezar","family":"Ionescu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrik","family":"Jansson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,11,16]]},"reference":[{"key":"9_CR1","unstructured":"Agda wiki page. http:\/\/wiki.portal.chalmers.se\/agda\/"},{"key":"9_CR2","unstructured":"Formalisation of Mathematics. http:\/\/wiki.portal.chalmers.se\/cse\/pmwiki.php\/ForMath\/ForMath"},{"key":"9_CR3","unstructured":"GEM-E3 Website. http:\/\/www.gem-e3.net\/"},{"key":"9_CR4","unstructured":"ReMIND-R. http:\/\/www.pik-potsdam.de\/research\/sustainable-solutions\/models\/remind"},{"key":"9_CR5","volume-title":"Dynamic Programming","author":"RE Bellman","year":"1957","unstructured":"Bellman, R.E.: Dynamic Programming. Princeton University Press, Princeton (1957)"},{"key":"9_CR6","volume-title":"Dynamic Programming and Optimal Control","author":"DP Bertsekas","year":"2000","unstructured":"Bertsekas, D.P.: Dynamic Programming and Optimal Control, 2nd edn. Athena Scientific, Belmont (2000)","edition":"2"},{"key":"9_CR7","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/FI-2010-303","volume":"102","author":"E Brady","year":"2010","unstructured":"Brady, E., Hammond, K.: Correct-by-construction concurrency: using dependent types to verify implementations of effectful resource usage protocol. Fundamenta Informaticae 102, 145\u2013176 (2010)","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"9_CR8","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/BF01933419","volume":"8","author":"EW Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: A constructive approach to the problem of program correctness. BIT Numer. Math. 8(3), 174\u2013186 (1968)","journal-title":"BIT Numer. Math."},{"key":"9_CR9","unstructured":"Evensen, P., M\u00e4rdin, M.: An extensible and scalable agent-based simulation of barter economics. Master\u2019s thesis 2009\/04a, Chalmers University of Technology and University of Gothenburg (2009)"},{"issue":"1","key":"9_CR10","first-page":"13","volume":"6","author":"H Gintis","year":"2006","unstructured":"Gintis, H.: The emergence of a price system from decentralized bilateral exchange. B.E. J. Theor. Econ. 6(1), 13 (2006)","journal-title":"B.E. J. Theor. Econ."},{"issue":"13\u201316","key":"9_CR11","first-page":"645","volume":"6","author":"V Kreinovich","year":"2012","unstructured":"Kreinovich, V.: Designing, understanding, and analyzing unconventional computation: the important role of logic and constructive mathematics. Appl. Math. Sci. 6(13\u201316), 645\u2013649 (2012)","journal-title":"Appl. Math. Sci."},{"issue":"1522","key":"9_CR12","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1098\/rsta.1984.0073","volume":"312","author":"P Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. Philos. Trans. R. Soc. Lond. 312(1522), 501\u2013518 (1984)","journal-title":"Philos. Trans. R. Soc. Lond."},{"key":"9_CR13","unstructured":"McBride, C.: Dependently typed programming. http:\/\/www.cs.uoregon.edu\/Research\/summerschool\/summer10\/curriculum.htm"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1017\/S0956796809007345","volume":"19","author":"S-C Mu","year":"2009","unstructured":"Mu, S.-C., Ko, H.-S., Jansson, P.: Algebra of programming in Agda: dependent types for relational program derivation. J. Funct. Program. 19, 545\u2013579 (2009)","journal-title":"J. Funct. Program."},{"key":"9_CR15","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"B Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin-L\u00f6f\u2019s Type Theory. Oxford University Press, Oxford (1990)"},{"key":"9_CR16","first-page":"1","volume-title":"In: Handbook of Logic in Computer Science","author":"B Nordstr\u00f6m","year":"2000","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Martin-L\u00f6f type theory. In: Handbook of Logic in Computer Science, vol. 5, pp. 1\u201337. Oxford University Press, Oxford (2000)"},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/BF02136027","volume":"24","author":"B Nordstr\u00f6m","year":"1984","unstructured":"Nordstr\u00f6m, B., Smith, J.: Propositions and specifications of programs in Martin-L\u00f6f\u2019s type theory. BIT Numer. Math. 24, 288\u2013301 (1984)","journal-title":"BIT Numer. Math."},{"key":"9_CR18","volume-title":"Introduction to Logic. Dover Books on Mathematics Series","author":"P Suppes","year":"1999","unstructured":"Suppes, P.: Introduction to Logic. Dover Books on Mathematics Series. Dover, New York (1999). (Reprint of the 1957 edition from Van Nostrand)"},{"key":"9_CR19","first-page":"440","volume-title":"TPHOLs 2009. LNCS","author":"W Swierstra","year":"2009","unstructured":"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\u2013451. Springer, Heidelberg (2009)"},{"key":"9_CR20","volume-title":"Type Theory and Functional Programming","author":"S Thompson","year":"1991","unstructured":"Thompson, S.: Type Theory and Functional Programming. Addison-Wesley, Redwood (1991)"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Thompson, S.: Are subsets necessary in Martin-L\u00f6f type theory? In: Myers Jr, J.P., O\u2019Donnell, M.J. (eds.) Constructivity in CS 1991. LNCS, vol. 613. Springer, Heidelberg (1992)","DOI":"10.1007\/BFb0021082"},{"key":"9_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-052-4","volume-title":"Computable Models","author":"R Turner","year":"2009","unstructured":"Turner, R.: Computable Models. Springer, London (2009)"},{"key":"9_CR23","volume-title":"Microeconomic Analysis","author":"HR Varian","year":"1992","unstructured":"Varian, H.R.: Microeconomic Analysis. Norton, New York (1992)"},{"key":"9_CR24","doi-asserted-by":"publisher","DOI":"10.1093\/0198295278.001.0001","volume-title":"Computable Economics: The Arne Ryde Memorial Lectures","author":"K Velupillai","year":"2000","unstructured":"Velupillai, K.: Computable Economics: The Arne Ryde Memorial Lectures. Oxford University Press, Oxford (2000)"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1016\/j.amc.2005.11.113","volume":"179","author":"KV Velupillai","year":"2006","unstructured":"Velupillai, K.V.: Algorithmic foundations of computable general equilibrium theory. Appl. Math. Comput. 179, 360\u2013369 (2006)","journal-title":"Appl. Math. Comput."},{"issue":"01","key":"9_CR26","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1142\/S1793005712400017","volume":"8","author":"KV Velupillai","year":"2012","unstructured":"Velupillai, K.V.: Taming the incomputable, reconstructing the nonconstructive and deciding the undecidable in mathematical economics. New Math. Nat. Comput. (NMNC) 8(01), 5\u201351 (2012)","journal-title":"New Math. Nat. Comput. (NMNC)"},{"key":"9_CR27","volume-title":"Elements of Pure Economics: Or the Theory of Social Wealth. Routledge Library Editions-Economics","author":"L Walras","year":"1954","unstructured":"Walras, L.: Elements of Pure Economics: Or the Theory of Social Wealth. Routledge Library Editions-Economics. Taylor & Francis Group, London (1954)"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Functional Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41582-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,14]],"date-time":"2023-02-14T08:26:03Z","timestamp":1676363163000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-41582-1_9"}},"subtitle":["Examples from Economic Modelling"],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642415814","9783642415821"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41582-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"16 November 2013","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}