{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:54:19Z","timestamp":1725515659873},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313738"},{"type":"electronic","value":"9783642313745"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_13","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"186-201","source":"Crossref","is-referenced-by-count":2,"title":["An Essence of SSReflect"],"prefix":"10.1007","author":[{"given":"Iain","family":"Whiteside","sequence":"first","affiliation":[]},{"given":"David","family":"Aspinall","sequence":"additional","affiliation":[]},{"given":"Gudmund","family":"Grov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s11786-010-0025-6","volume":"3","author":"D. Aspinall","year":"2010","unstructured":"Aspinall, D., Denney, E., L\u00fcth, C.: Tactics for hierarchical proof. Mathematics in Computer Science\u00a03, 309\u2013330 (2010)","journal-title":"Mathematics in Computer Science"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-14052-5_9","volume-title":"Interactive Theorem Proving","author":"S. Autexier","year":"2010","unstructured":"Autexier, S., Dietrich, D.: A Tactic Language for Declarative Proofs. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 99\u2013114. Springer, Heidelberg (2010)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-68103-8_5","volume-title":"Types for Proofs and Programs","author":"P. Corbineau","year":"2008","unstructured":"Corbineau, P.: A Declarative Language for the Coq Proof Assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 69\u201384. Springer, Heidelberg (2008)"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/j.entcs.2005.11.063","volume":"155","author":"E. Denney","year":"2006","unstructured":"Denney, E., Power, J., Tourlas, K.: Hiproofs: A hierarchical notion of proof tree. Electr. Notes Theor. Comput. Sci.\u00a0155, 341\u2013359 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Barendregt, H., et al.: Lambda calculi with types. In: Handbook of Logic in Computer Science, pp. 117\u2013309. Oxford University Press (1992)","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"13_CR6","unstructured":"Fowler, M.: Refactoring: improving the design of existing code. Addison-Wesley (1999)"},{"key":"13_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-87827-8_28","volume-title":"Computer Mathematics","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: The Four Colour Theorem: Engineering of a Formal Proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol.\u00a05081, p. 333. Springer, Heidelberg (2008)"},{"key":"13_CR8","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Th\u00e9ry, L.: A Modular Formalisation of Finite Group Theory. Rapport de recherche RR-6156, INRIA (2007)"},{"key":"13_CR9","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA (2008)"},{"key":"13_CR10","unstructured":"Gonthier, G., St\u00e9phane Le, R.: An Ssreflect Tutorial. Technical Report RT-0367, INRIA (2009)"},{"issue":"1-2","key":"13_CR11","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-009-9137-6","volume":"44","author":"F. Guidi","year":"2010","unstructured":"Guidi, F.: Procedural representation of cic proof terms. J. Autom. Reason.\u00a044(1-2), 53\u201378 (2010)","journal-title":"J. Autom. Reason."},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/BFb0097791","volume-title":"Types for Proofs and Programs","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Proof Style. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, pp. 154\u2013172. Springer, Heidelberg (1998)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-22673-1_3","volume-title":"Intelligent Computer Mathematics","author":"J. Heras","year":"2011","unstructured":"Heras, J., Poza, M., D\u00e9n\u00e8s, M., Rideau, L.: Incidence Simplicial Matrices Formalized in Coq\/SSReflect. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS, vol.\u00a06824, pp. 30\u201344. Springer, Heidelberg (2011)"},{"key":"13_CR14","unstructured":"Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq proof assistant: A tutorial (August 2007)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Komendantsky, V.: Reflexive toolbox for regular expression matching: verification of functional programs in Coq+SSReflect. In: PLPV 2012, pp. 61\u201370 (2012)","DOI":"10.1145\/2103776.2103784"},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1109\/TSE.2004.1265817","volume":"30","author":"T. Mens","year":"2004","unstructured":"Mens, T., Tourwe, T.: A survey of software refactoring. IEEE Trans. Softw. Eng.\u00a030(2), 126\u2013139 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1-2","key":"13_CR17","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10817-009-9136-7","volume":"44","author":"C. Sacerdoti Coen","year":"2010","unstructured":"Sacerdoti Coen, C.: Declarative representation of proof terms. J. Autom. Reason.\u00a044(1-2), 25\u201352 (2010)","journal-title":"J. Autom. Reason."},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 - A Generic Interpretative Approach to Readable Formal Proof Documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013184. Springer, Heidelberg (1999)"},{"key":"13_CR19","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-22673-1_18","volume-title":"Intelligent Computer Mathematics","author":"I. Whiteside","year":"2011","unstructured":"Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards Formal Proof Script Refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS (LNAI), vol.\u00a06824, pp. 260\u2013275. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31374-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,26]],"date-time":"2024-04-26T01:55:18Z","timestamp":1714096518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}