{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:57:45Z","timestamp":1776553065641,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540617808","type":"print"},{"value":"9783540707226","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_73","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:25:14Z","timestamp":1330295114000},"page":"231-248","source":"Crossref","is-referenced-by-count":4,"title":["Context-relative syntactic categories and the formalization of mathematical text"],"prefix":"10.1007","author":[{"given":"Aarne","family":"Ranta","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, pages 381\u2013392, 1972. Reprinted in R. Nederpelt, editor, Selected Papers on Automath, pages 375\u2013388. North-Holland, Amsterdam, 1994.","journal-title":"Indagationes Mathematicae"},{"key":"16_CR2","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1016\/S0049-237X(08)70231-3","volume-title":"Selected Papers on Automath","author":"N.G. Bruijn de","year":"1994","unstructured":"N.G. de Bruijn. The mathematical vernacular, a language for mathematics with typed sets. R. Nederpelt, editor, Selected Papers on Automath, pages 865\u2013935. North-Holland, Amsterdam, 1994."},{"key":"16_CR3","volume-title":"Rapport de recherche n.2459","author":"Y. Coscoy","year":"1995","unstructured":"Yann Coscoy, Gilles Kahn and Laurent Th\u00e9ry. Extracting text from proofs. Rapport de recherche n.2459, INRIA, Sophia-Antipolis, 1995."},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science 806","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-58085-9_78","volume-title":"Types for Proofs and Programs","author":"L. Magnusson","year":"1994","unstructured":"Lena Magnusson and Bengt Nordstr\u00f6m. The ALF Proof Editor and Its Proof Engine. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, pages 213\u2013237. Lecture Notes in Computer Science 806, Springer-Verlag, Heidelberg, 1994."},{"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":"Type Theoretical Grammar","author":"A. Ranta","year":"1994","unstructured":"Aarne Ranta. Type Theoretical Grammar. Oxford University Press, Oxford, 1994."},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science 996","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-60579-7_9","volume-title":"Types for Proofs and Programs","author":"A. Ranta","year":"1995","unstructured":"Aarne Ranta. Syntactic categories in the language of mathematics. In P. Dybjer, B. Nordstr\u00f6m, and J. Smith, editors, Types for Proofs and Programs, pages 162\u2013182, Lecture Notes in Computer Science 996, Springer-Verlag, Heidelberg, 1995."}],"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-61780-9_73.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:36:43Z","timestamp":1619573803000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_73"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_73","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}