{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,5,4]],"date-time":"2022-05-04T10:26:26Z","timestamp":1651659986436},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T00:00:00Z","timestamp":1245974400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2010,2]]},"DOI":"10.1007\/s10817-009-9136-7","type":"journal-article","created":{"date-parts":[[2009,6,25]],"date-time":"2009-06-25T11:36:12Z","timestamp":1245929772000},"page":"25-52","source":"Crossref","is-referenced-by-count":7,"title":["Declarative Representation of Proof Terms"],"prefix":"10.1007","volume":"44","author":[{"given":"Claudio","family":"Sacerdoti Coen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,6,26]]},"reference":[{"key":"9136_CR1","unstructured":"The Coq Development Team: The Coq proof assistant reference manual (2005)"},{"issue":"2","key":"9136_CR2","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A Asperti","year":"2007","unstructured":"Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. J. Autom. Reason. 39(2), 109\u2013139 (2007)","journal-title":"J. Autom. Reason."},{"key":"9136_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/11618027_16","volume-title":"Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005","author":"C Sacerdoti Coen","year":"2006","unstructured":"Sacerdoti Coen, C.: Explanation in natural language of lambda-bar-mu-mu-tilde-terms. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005. Lecture Notes in Computer Science, vol.\u00a03863, pp.\u00a0234\u2013249. Springer, New York (2006)"},{"key":"9136_CR4","series-title":"Lectures Notes in Artificial Intelligence","first-page":"67","volume-title":"Proceedings of Mathematical Knowledge Management 2006","author":"S Autexier","year":"2006","unstructured":"Autexier, S., Sacerdoti Coen, C.: A formal correspondence between omdoc with alternative proofs and the lambda-bar-mu-mu-tilde-calculus. In: Proceedings of Mathematical Knowledge Management 2006. Lectures Notes in Artificial Intelligence, vol.\u00a04108, pp.\u00a067\u201381. Springer, New York (2006)"},{"key":"9136_CR5","doi-asserted-by":"crossref","unstructured":"Guidi, F.: Procedural representation of CIC proof terms. J. Autom. Reason. (2009). doi: 10.1007\/s10817-009-9137-6","DOI":"10.1007\/s10817-009-9137-6"},{"key":"9136_CR6","unstructured":"Raffalli, C.: The proof checker documentation, version 0.85, manual of the PhoX proof assistant (2005)"},{"key":"9136_CR7","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar\u2014a generic interpretative approach to readable formal proof documents. In: Theorem Proving in Higher Order Logics. LNCS, vol. 1690, pp. 167\u2013184. Springer, New York (1999)"},{"issue":"3\u20134","key":"9136_CR8","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1023\/A:1021935419355","volume":"29","author":"M Wenzel","year":"2002","unstructured":"Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3\u20134), 389\u2013411 (2002)","journal-title":"J. Autom. Reason."},{"key":"9136_CR9","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"125","volume-title":"Proceedings of User Interface for Theorem Provers 2006","author":"C Sacerdoti Coen","year":"2006","unstructured":"Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: Tinycals: step by step tacticals. In: Proceedings of User Interface for Theorem Provers 2006. Electronic Notes in Theoretical Computer Science, vol. 174, pp. 125\u2013142. Elsevier, Amsterdam (2006)"},{"key":"9136_CR10","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: A Mizar mode for HOL. In: von Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996. LNCS, vol. 1125, pp. 203\u2013220. Springer, New York (1996)"},{"key":"9136_CR11","unstructured":"Sacerdoti Coen, C.: Tactics in modern proof-assistants: the bad habit of overkilling. In: Supplementary Proceedings of the 14th International Conference TPHOLS 2001, pp. 352\u2013367 (2001)"},{"key":"9136_CR12","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/351240.351262","volume-title":"ICFP \u201900: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming","author":"PL Curien","year":"2000","unstructured":"Curien, P.L., Herbelin, H.: The duality of computation. In: ICFP \u201900: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp. 233\u2013243. ACM, New York (2000). doi: http:\/\/doi.acm.org\/10.1145\/351240.351262"},{"key":"9136_CR13","unstructured":"Kirchner, F., Sacerdoti Coen, C.: The Fellowship Super-prover. http:\/\/www.lix.polytechnique.fr\/Labo\/Florent.Kirchner\/fellowship\/ (2008)"},{"key":"9136_CR14","unstructured":"Kirchner, F.: Interoperable proof systems. Ph.D. thesis, \u00c9cole Polytechnique (2007)"},{"key":"9136_CR15","unstructured":"Asperti, A., Loeb, I., Sacerdoti Coen, C.: Stylesheets to intermediate representation and presentational stylesheets. MoWGLI Report D2d,D2f (2003)"},{"key":"9136_CR16","unstructured":"Asperti, A., Tassi, E.: An interactive driver for goal directed proof strategies. In: Proc. of User Interfaces for Theorem Provers 2008, Montreal (2008)"},{"key":"9136_CR17","unstructured":"Coscoy, Y., Kahn, G., Thery, L.: Extracting text from proofs. Technical Report RR-2459, Inria (Institut National de Recherche en Informatique et en Automatique), France (1995)"},{"key":"9136_CR18","series-title":"LNCS","volume-title":"TYPES 2007: Types for Proof and Programs","author":"P Corbineau","year":"2008","unstructured":"Corbineau, P.: A declarative proof language for the Coq proof assistant. In: TYPES 2007: Types for Proof and Programs. LNCS, vol. 4941. Springer, New York (2008)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9136-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9136-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9136-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:49Z","timestamp":1559265709000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9136-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,26]]},"references-count":18,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["9136"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9136-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,6,26]]}}}