{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:58:28Z","timestamp":1725551908351},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540314301"},{"type":"electronic","value":"9783540314318"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11618027_26","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T11:48:07Z","timestamp":1137671287000},"page":"389-403","source":"Crossref","is-referenced-by-count":1,"title":["Translating a Fragment of Weak Type Theory into Type Theory with Open Terms"],"prefix":"10.1007","author":[{"given":"G. I.","family":"Jojgov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"The Coq Development\u00a0Team. The Coq Proof Assistant Reference Manual \u2013 Version V8 (2004), http:\/\/coq.inria.fr\/"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/3-540-45793-3_36","volume-title":"Computer Science Logic","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Jojgov, G.: Open Proofs and Open Terms: a Basis for Interactive Logic. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 537\u2013552. Springer, Heidelberg (2002)"},{"key":"26_CR3","unstructured":"Jojgov, G.I.: Incomplete Proofs and Terms and Their Use in Interactive Theorem Proving. PhD thesis, Eindhoven University of Technology (2004)"},{"key":"26_CR4","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 (2001)","DOI":"10.1023\/A:1011286100450"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Kamareddine, F., Maarek, M., Wells, J.B.: Mathlang: Experience-driven development of a new mathematical language. In: MKM Symposium 2003. Elsevier, Amsterdam (2003)","DOI":"10.1016\/j.entcs.2003.12.032"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-27818-4_12","volume-title":"Mathematical Knowledge Management","author":"F. Kamareddine","year":"2004","unstructured":"Kamareddine, F., Maarek, M., Wells, J.B.: Flexible encoding of mathematics on the computer. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"26_CR7","unstructured":"McBride, C.: Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh (1999)"},{"key":"26_CR8","unstructured":"Nederpelt, R.: Weak Type Theory: A formal language for mathematics. Technical report, Eindhoven University of Technology (May 2002)"},{"key":"26_CR9","series-title":"Studies in Logic and Foundations of Mathematics","volume-title":"Selected Papers on Automath","year":"1994","unstructured":"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)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/3-540-39185-1_15","volume-title":"Types for Proofs and Programs","author":"T. Nipkow","year":"2003","unstructured":"Nipkow, T.: Structured Proofs in Isar\/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 259\u2013278. Springer, Heidelberg (2003)"},{"key":"26_CR11","unstructured":"Paulson, L.: Introduction to Isabelle. Technical report, University of Cambridge (1993)"},{"key":"26_CR12","unstructured":"Ranta, A.: Grammatical Framework: A Type-Theoretical Grammar Formalism. Journal of Functional Programming (2003)"},{"key":"26_CR13","unstructured":"Rudnicki, P.: An overview of the Mizar project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs (1992), http:\/\/www.mizar.org"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Thery, L.: Colouring Proofs: A Lightweight Approach to Adding Formal Structure to Proofs. In: Proceedings of User Interfaces for Theorem Provers UITP 2003. ENTCS 103 (2003)","DOI":"10.1016\/j.entcs.2004.07.002"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","author":"M. Wenzel","year":"2002","unstructured":"Wenzel, M., Nipkow, T., Paulson, L.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-24849-1_24","volume-title":"Types for Proofs and Programs","author":"F. Wiedijk","year":"2004","unstructured":"Wiedijk, F.: Formal Proof Sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 378\u2013393. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11618027_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T06:42:57Z","timestamp":1683355377000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11618027_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540314301","9783540314318"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11618027_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}