{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:31:55Z","timestamp":1759847515688},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540580850"},{"type":"electronic","value":"9783540484400"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58085-9_84","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:11:16Z","timestamp":1330269076000},"page":"352-365","source":"Crossref","is-referenced-by-count":5,"title":["Type theory and the informal language of mathematics"],"prefix":"10.1007","author":[{"given":"Aarne","family":"Ranta","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"16_CR1","unstructured":"N. G. de Bruijn. Formalizing the mathematical vernacular. Technical report, Eindhoven University of Technology, 1982."},{"key":"16_CR2","doi-asserted-by":"crossref","DOI":"10.1515\/9783112316009","volume-title":"Syntactic Structures","author":"N. Chomsky","year":"1957","unstructured":"Noam Chomsky. Syntactic Structures. Mouton, The Hague, 1957."},{"key":"16_CR3","volume-title":"Begriffsschrift","author":"G. Frege","year":"1879","unstructured":"Gottlob Frege. Begriffsschrift. Louis Nebert, Halle A\/S, 1879. In English, van Heijenoort 1967."},{"key":"16_CR4","volume-title":"Grundlagen der Geometrie","author":"D. Hilbert","year":"1903","unstructured":"David Hilbert. Grundlagen der Geometrie. Teubner, Leipzig, 2nd edition, 1903. 1st ed. 1899.","edition":"2nd edition"},{"key":"16_CR5","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, Naples, 1984."},{"key":"16_CR6","volume-title":"Formal Philosophy","author":"R. Montague","year":"1974","unstructured":"Richard Montague. Formal Philosophy. Yale University Press, New Haven, 1974. Collected papers edited by Richmond Thomason."},{"key":"16_CR7","volume-title":"Programming in Martin-L\u00f6f's Type Theory. An Introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan Smith. Programming in Martin-L\u00f6f's Type Theory. An Introduction. Clarendon Press, Oxford, 1990."},{"key":"16_CR8","unstructured":"Jan von Plato. The axioms of constructive geometry. Manuscript, University of Helsinki, 1994. To appear."},{"key":"16_CR9","volume-title":"Type Theoretical Grammar","author":"A. Ranta","year":"1994","unstructured":"Aarne Ranta. Type Theoretical Grammar. Oxford University Press, Oxford, 1994. To appear."},{"key":"16_CR10","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BF00627403","volume":"14","author":"A. Ranta","year":"1991","unstructured":"Aarne Ranta. Intuitionistic categorial grammar. Linguistics and Philosophy, 14:203\u2013239, 1991.","journal-title":"Linguistics and Philosophy"},{"key":"16_CR11","first-page":"483","volume-title":"Formal Methods in the Study of Language, Part 2","author":"R. Scha","year":"1981","unstructured":"Remko Scha. Distributive, collective and cumulative quantification. In J. Groenendijk, T. Janssen, and M. Stokhof, editors, Formal Methods in the Study of Language, Part 2, pages 483\u2013517. Mathematisch Centrum, Amsterdam, 1981."},{"key":"16_CR12","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1007\/978-94-009-5203-4_8","volume-title":"Handbook of Philosophical Logic, Vol. III","author":"G. Sundholm","year":"1986","unstructured":"G\u00f6ran Sundholm. Proof theory and meaning. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Vol. III, pages 471\u2013506. D. Reidel, Dordrecht, 1986."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58085-9_84.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:10:49Z","timestamp":1619572249000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58085-9_84"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540580850","9783540484400"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-58085-9_84","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}