{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T11:12:27Z","timestamp":1791025947736,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425250","type":"print"},{"value":"9783540447559","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_25","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:03:32Z","timestamp":1186740212000},"page":"362-377","source":"Crossref","is-referenced-by-count":7,"title":["Experiments with Finite Tree Automata in Coq"],"prefix":"10.1007","author":[{"given":"Xavier","family":"Rival","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean","family":"Goubault-Larrecq","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"25_CR1","volume-title":"Technical report","author":"B. Barras","year":"1999","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliatre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saibi, and B. Werner. The Coq proof assistant reference manual: Version 6.3.1. Technical report, INRIA, France, 1999."},{"key":"25_CR2","series-title":"Lect Notes Comput Sci","volume-title":"TACS\u201997","author":"S. Boutin","year":"1997","unstructured":"S. Boutin. Using reflection to build efficient and certified decision procedures. In M. Abadi and T. Ito, editors, TACS\u201997. Springer-Verlag LNCS 1281, 1997."},{"key":"25_CR3","unstructured":"R. Boyer and J. S. Moore. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In The Correctness Problem in Computer Science. Acad. Press, 1981."},{"key":"25_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/BFb0054183","volume-title":"TACAS\u201998","author":"W. Charatonik","year":"1998","unstructured":"W. Charatonik and A. Podelski. Set-based analysis of reactive infinite-state systems. In B. Steffen, editor, TACAS\u201998, pages 358\u2013375. Springer Verlag LNCS 1384, 1998."},{"key":"25_CR5","unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, T. Sophie, and M. Tommasi. Tree automata techniques and applications. Available at http:\/\/www.grappa.univ-lille3.fr\/tata , 1997."},{"issue":"6","key":"25_CR6","first-page":"837","volume":"13","author":"L. Fribourg","year":"1994","unstructured":"L. Fribourg and M. Veloso Peixoto. Automates concurrents \u00e0 contraintes. Technique et Science Informatique, 13(6):837\u2013866, 1994.","journal-title":"Technique et Science Informatique"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"F. G\u00e9cseg and M. Steinby. Tree languages. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3, pages 1\u201368. Springer Verlag, 1997.","DOI":"10.1007\/978-3-642-59126-6_1"},{"key":"25_CR8","unstructured":"J. Goubault-Larrecq. Satisfiability of inequality constraints and detection of cycles with negative weight in graphs. Part of the Coq contribs, available at http:\/\/pauillac.inria.fr\/coq\/contribs\/graphs.html , 1998."},{"key":"25_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"977","DOI":"10.1007\/3-540-45591-4_134","volume-title":"FMPPTA\u20192000","author":"J. Goubault-Larrecq","year":"2000","unstructured":"J. Goubault-Larrecq. A method for automatic cryptographic protocol verification. In FMPPTA\u20192000, pages 977\u2013984. Springer Verlag LNCS 1800, 2000."},{"key":"25_CR10","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1093\/comjnl\/38.2.162","volume":"38","author":"J. Harrison","year":"1995","unstructured":"J. Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162\u2013170, 1995.","journal-title":"The Computer Journal"},{"key":"25_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/BFb0105407","volume-title":"TPHOL\u201996","author":"J. Harrison","year":"1996","unstructured":"J. Harrison. St\u00e5lmarck\u2019s algorithm as a HOL derived rule. In J. von Wright, J. Grundy, and J. Harrison, editors, TPHOL\u201996, pages 221\u2013234. Springer Verlag LNCS 1125, 1996."},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud. Rewrite proofs and computations. In H. Schwichtenberg, editor, Proof and Computation, volume 139 of NATO series F: Computer and Systems Sciences, pages 173\u2013218. Springer Verlag, 1995.","DOI":"10.1007\/978-3-642-79361-5_7"},{"key":"25_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/3-540-48294-6_10","volume-title":"SAS\u201999","author":"D. Monniaux","year":"1999","unstructured":"D. Monniaux. Abstracting cryptographic protocols with tree automata. In SAS\u201999, pages 149\u2013163. Springer Verlag LNCS 1694, 1999."},{"key":"25_CR14","unstructured":"O. M\u00fcller. A verification environment for I\/O automata based on formalized meta-theory. Master\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen, 1998."},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 4, pages 133\u2013191. Elsevier Science Publishers B. V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"25_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-44464-5_13","volume-title":"ASIAN\u20192000","author":"K. N. Verma","year":"2000","unstructured":"K. N. Verma, J. Goubault-Larrecq, S. Prasad, and S. Arun-Kumar. Reflecting BDDs in Coq. In ASIAN\u20192000, pages 162\u2013181. Springer Verlag LNCS 1961, 2000."},{"issue":"1 2","key":"25_CR17","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","volume":"13","author":"R. W. Weyhrauch","year":"1980","unstructured":"R. W. Weyhrauch. Prolegomena to a theory of mechanized formal reasoning. Artifical Intelligence, 13(1, 2):133\u2013170, 1980.","journal-title":"Artifical Intelligence"},{"key":"25_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"442","DOI":"10.1007\/3-540-63533-5_23","volume-title":"FME\u201997","author":"S. Yu","year":"1997","unstructured":"S. Yu and Z. Luo. Implementing a model checker for LEGO. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME\u201997, pages 442\u2013458. Springer-Verlag LNCS 1313, 1997."}],"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-44755-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T22:10:34Z","timestamp":1556748634000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}