{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:36:37Z","timestamp":1742960197312,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230298"},{"type":"electronic","value":"9783540278184"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27818-4_11","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T14:26:47Z","timestamp":1267108007000},"page":"145-159","source":"Crossref","is-referenced-by-count":3,"title":["A Path to Faithful Formalizations of Mathematics"],"prefix":"10.1007","author":[{"given":"Gueorgui","family":"Jojgov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rob","family":"Nederpelt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, et al. (eds.) Handbook of Logic in Computer Science, pp. 117\u2013309. Oxford University Press, Oxford (1992)"},{"key":"11_CR2","volume-title":"Handbook of Automated Reasoning","author":"H. Barendregt","year":"1999","unstructured":"Barendregt, H., Geuvers, H.: Proof assistants using dependent type systems. In: Handbook of Automated Reasoning. Elsevier Science Publishers B.V., Amsterdam (1999)"},{"key":"11_CR3","series-title":"Studies in Logic and Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1016\/S0049-237X(08)70222-2","volume-title":"Selected Papers on Automath","author":"L.S. Benthem Jutting van","year":"1994","unstructured":"van Benthem Jutting, L.S.: Checking Landau\u2019s \u201cGrundlagen\u201d in the Automath System. In: Nederpelt, R.P., Geuvers, J.H., de Vrijer, R.C. (eds.) Selected Papers on Automath. Studies in Logic and Foundations of Mathematics, vol.\u00a0133, pp. 701\u2013732. North-Holland, Amsterdam (1994)"},{"key":"11_CR4","series-title":"Studies in Logic and Foundations of Mathematics","volume-title":"Selected Papers on Automath","author":"N.G. Bruijn de","year":"1994","unstructured":"de Bruijn, N.G.: The mathematical language Automath, its usage and some of its extensions. In: Nederpelt, R.P., Geuvers, J.H., de Vrijer, R.C. (eds.) Selected Papers on Automath. Studies in Logic and Foundations of Mathematics, vol.\u00a0133. North-Holland, Amsterdam (1994)"},{"unstructured":"The Coq Development Team, The Coq Proof Assistant Reference Manual - Version V7.4 (February 2003), \n                  \n                    http:\/\/coq.inria.fr\/","key":"11_CR5"},{"unstructured":"Jojgov, G.I.: Incomplete Proofs and Terms and Their Use in Interactive Theorem Proving, PhD thesis. Eindhoven University of Technology (2004)","key":"11_CR6"},{"key":"11_CR7","volume-title":"Proceedings of the MKM Symposium 2003","author":"G.I. Jojgov","year":"2003","unstructured":"Jojgov, G.I., Nederpelt, R.P., Scheffer, M.: Faithfully reflecting the structure of informal mathematical proofs into formal type theories. In: Proceedings of the MKM Symposium 2003. Elsevier, Amsterdam (2003)"},{"doi-asserted-by":"crossref","unstructured":"Kamareddine, F., Nederpelt, R.: A refinement of de Bruijn\u2019s formal language of mathematics. Journal of Logic, Language and Information (to appear)","key":"11_CR8","DOI":"10.1023\/B:JLLI.0000028393.47593.b8"},{"unstructured":"Nederpelt, R.: Weak Type Theory: A formal language for mathematics, Technical report. Eindhoven University of Technology (May 2002)","key":"11_CR9"},{"unstructured":"Pollack, R.: The LEGO Proof Assistant, \n                  \n                    http:\/\/www.dcs.ed.ac.uk\/home\/lego\/index.html","key":"11_CR10"},{"unstructured":"Rudnicki, P.: An overview of the Mizar project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs (1992), \n                  \n                    http:\/\/www.mizar.org","key":"11_CR11"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27818-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,12]],"date-time":"2019-03-12T09:54:09Z","timestamp":1552384449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27818-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230298","9783540278184"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27818-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}