{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T05:37:23Z","timestamp":1737610643694,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665366"},{"type":"electronic","value":"9783540481683"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48168-0_31","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T11:30:26Z","timestamp":1196508626000},"page":"439-452","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Safe Proof Checking in Type Theory with Y"],"prefix":"10.1007","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[]},{"given":"Erik","family":"Poll","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Zwanenburg","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"P. Audebaud, Partial Objects in the Calculus of Constructions, in Proceedings of the Sixth Annual Symp. on Logic in Computer Science, Amsterdam 1991, IEEE, pp. 86\u201395.","DOI":"10.1109\/LICS.1991.151633"},{"key":"31_CR2","unstructured":"H.P. Barendregt, Lambda calculi with Types. In Handbook of Logic in Computer Science, eds. Abramski et al., Oxford Univ. Press, pp. 117\u2013309."},{"key":"31_CR3","unstructured":"S. Berardi, Type dependence and constructive mathematics, Ph.D. thesis, Universita di Torino, Italy."},{"key":"31_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88: International conference on computer logic","author":"Th. Coquand","year":"1990","unstructured":"Th. Coquand and Ch. Paulin-Mohring Inductively defined types, In P. Martin-L\u00f6f and G. Mints editors. COLOG-88: International conference on computer logic, LNCS 417."},{"key":"31_CR5","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, Ch. Paulin-Mohring, B. Werner, The Coq proof assistant version 5.6, user\u2019s guide. INRIA Rocquencourt-CNRS ENS Lyon."},{"key":"31_CR6","unstructured":"H. Geuvers, Logics and Type Systems, Ph.D. Thesis, University of Nijmegen, 1993."},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"J.H. Geuvers and M.J. Nederhof, A modular proof of strong normalisation for the calculus of constructions. Journal of Functional Programming, vol 1 (2), pp 155\u2013189.","DOI":"10.1017\/S0956796800020037"},{"key":"31_CR8","volume-title":"Manuscript, Faculty of Mathematics and Computer Science","author":"J. Terlouw","year":"1989","unstructured":"J. Terlouw, Een nadere bewijstheoretische analyse van GSTT\u2019s (incl. appendix), Manuscript, Faculty of Mathematics and Computer Science, University of Nijmegen, Netherlands, March, April 1989. (In Dutch)"},{"key":"31_CR9","unstructured":"J. Zwanenburg and H. Geuvers, Example of Proof Search by iteration in Coq, url: http:\/\/www.cs.kun.nl\/~janz\/proofs\/proofSearch\/index.html"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48168-0_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T03:46:05Z","timestamp":1737603965000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"13 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}