{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T00:36:37Z","timestamp":1794357397086,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540851097","type":"print"},{"value":"9783540851103","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85110-3_30","type":"book-chapter","created":{"date-parts":[[2008,7,26]],"date-time":"2008-07-26T02:00:32Z","timestamp":1217037632000},"page":"339-354","source":"Crossref","is-referenced-by-count":2,"title":["A Tactic Language for Hiproofs"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ewen","family":"Denney","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"30_CR1","series-title":"Electronic Notes in Theoretical Computer Science (ENTCS)","volume-title":"Proceedings of Mathematical Foundations of Programing Semantics (MFPS)","author":"E. Denney","year":"2005","unstructured":"Denney, E., Power, J., Tourlas, K.: Hiproofs: A hierarchical notion of proof tree. In: Proceedings of Mathematical Foundations of Programing Semantics (MFPS). Electronic Notes in Theoretical Computer Science (ENTCS). Elsevier, Amsterdam (2005)"},{"issue":"1","key":"30_CR2","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/s00165-003-0003-8","volume":"15","author":"M.V.M. Oliveira","year":"2003","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: ArcAngel: a tactic language for refinement. Formal Aspects of Computing\u00a015(1), 28\u201347 (2003)","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"30_CR3","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.entcs.2006.09.026","volume":"174","author":"C.S. Coen","year":"2007","unstructured":"Coen, C.S., Tassi, E., Zacchiroli, S.: Tinycals: Step by step tacticals. Electr. Notes Theor. Comput. Sci.\u00a0174(2), 125\u2013142 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/3-540-60579-7_8","volume-title":"Types for Proofs and Programs","author":"R. Pollack","year":"1995","unstructured":"Pollack, R.: On extensibility of proof checkers. In: Smith, J., Dybjer, P., Nordstr\u00f6m, B. (eds.) TYPES 1994. LNCS, vol.\u00a0996, pp. 140\u2013161. Springer, Heidelberg (1995)"},{"key":"30_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1017\/S0956796803004921","volume":"14","author":"A.W. Appel","year":"2004","unstructured":"Appel, A.W., Felty, A.P.: Dependent types ensure partial correctness of theorem provers. Journal of Functional Programming\u00a014, 3\u201319 (2004)","journal-title":"Journal of Functional Programming"},{"key":"30_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 85\u201395. Springer, Heidelberg (2000)"},{"key":"30_CR7","unstructured":"Kirchner, F.: Coq tacticals and PVS strategies: A small-step semantics. In: Archer, M., et al. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics. NASA, pp. 69\u201383 (September 2003)"},{"key":"30_CR8","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 \u2014 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":"30_CR9","unstructured":"Griffin, T.G.: Notational Definition and Top-down Refinement for Interactive Proof Development Systems. PhD thesis, Cornell University (1988)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85110-3_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:14:48Z","timestamp":1619507688000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85110-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851097","9783540851103"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85110-3_30","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-85110-3","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}