{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:09:36Z","timestamp":1725487776815},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_24","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"388-405","source":"Crossref","is-referenced-by-count":2,"title":["Formalizing St\u00e5lmarck\u2019s Algorithm in Coq"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Letouzey","sequence":"first","affiliation":[]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999","year":"1999","unstructured":"Yves Bertot, Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin, and Laurent Th\u00e9ry, editors. Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999, number 1690 in LNCS, Nice, France, 1999. Springer-Verlag."},{"key":"24_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/BFb0014048","volume-title":"Typed Lambda Calculus and its Applications","author":"Y. Coscoy","year":"1995","unstructured":"Yann Coscoy, Gilles Kahn, and Laurent Th\u00e9ry. Extracting text from proofs. In Typed Lambda Calculus and its Applications, volume 902 of LNCS, pages 109\u2013123. Springer-Verlag, 1995."},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","volume-title":"International Workshop, TYPES\u2019 98, Kloster Irsee, Germany","author":"J.-C. Filli\u00e2tre","year":"1998","unstructured":"J.-C. Filli\u00e2tre. Proof of Imperative Programs in Type Theory. In International Workshop, TYPES\u2019 98, Kloster Irsee, Germany, volume 1657 of LNCS. Springer-Verlag, March 1998."},{"key":"24_CR4","unstructured":"Michael J. C. Gordon and Thomas F. Melham. Introduction to HOL: a theorem proving environment for higher-order logic. Cambridge University Press, 1993."},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/BFb0105407","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996","author":"J. Harrison","year":"1996","unstructured":"J. Harrison. St\u00e5lmarck\u2019s algorithm as a HOL derived rule. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996, number 1125 in LNCS, pages 221\u2013234, Turku, Finland, August 1996. Springer-Verlag."},{"key":"24_CR6","unstructured":"G\u00e9rard Huet, Gilles Kahn, and Christine Paulin-Mohring. The Coq Proof Assistant: A Tutorial: Version 6.1. Technical Report 204, INRIA, 1997."},{"key":"24_CR7","unstructured":"Arndt Jonasson. Proof logging, definition of the log format. Prover Technology, December 1997."},{"key":"24_CR8","unstructured":"Xavier Leroy. Objective Caml. Available at \n                  http:\/\/pauillac.inria.fr\/ocaml\/\n                  \n                , 1997."},{"issue":"5\u20136","key":"24_CR9","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"Christine Paulin-Mohring and Benjamin Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15(5\u20136):607\u2013640, 1993.","journal-title":"Journal of Symbolic Computation"},{"key":"24_CR10","series-title":"Lect Notes Comput Sci","volume-title":"FMCAD\u2019 98","author":"M. Sheeran","year":"1998","unstructured":"Mary Sheeran and Gunnar St\u00e5lmarck. A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. In FMCAD\u2019 98, volume 1522 of LNCS. Springer-Verlag, November 1998."},{"key":"24_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/3-540-48256-3_14","volume-title":"Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999","author":"D. Syme","year":"1999","unstructured":"Don Syme. Three Tactic Theorem Proving. In Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin, and Laurent Th\u00e9ry, editors. Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999, number 1690 in LNCS, Nice, France, 1999. Springer-Verlag. Bertot et al. [1], pages 203\u2013220."},{"key":"24_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999","author":"M. Wenzel","year":"1999","unstructured":"Markus Wenzel. A Generic Interpretative Approach to Readable Formal Proof Documents. In Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin, and Laurent Th\u00e9ry, editors. Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999, number 1690 in LNCS, Nice, France, 1999. Springer-Verlag. Bertot et al. [1], pages 167\u2013184."},{"key":"24_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/3-540-48256-3_13","volume-title":"Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999","author":"V. Zammit","year":"1999","unstructured":"Vincent Zammit. On the Implementation of an Extensible Declarative Proof Language. In Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin, and Laurent Th\u00e9ry, editors. Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999, number 1690 in LNCS, Nice, France, 1999. Springer-Verlag. Bertot et al. [1], pages 185\u2013202."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T01:03:32Z","timestamp":1550451812000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}