{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T22:59:10Z","timestamp":1765666750152},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_14","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"173-188","source":"Crossref","is-referenced-by-count":4,"title":["Verified Decision Procedures on Context-Free Grammars"],"prefix":"10.1007","author":[{"given":"Yasuhiko","family":"Minamide","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Berstel, J.: Transductions and Context-Free Languages. Teubner Studienbucher (1979)","DOI":"10.1007\/978-3-663-09367-1"},{"issue":"9","key":"14_CR2","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1007\/s00236-002-0085-4","volume":"38","author":"J. Berstel","year":"2002","unstructured":"Berstel, J., Boasson, L.: Formal properties of XML grammars and languages. Acta Informatica\u00a038(9), 649\u2013671 (2002)","journal-title":"Acta Informatica"},{"key":"14_CR3","unstructured":"Courant, J., Filli\u00e2tre, J.-C.: Beginning of formal language theory (1993), http:\/\/coq.inria.fr\/contribs-eng.html"},{"key":"14_CR4","series-title":"ch. 3","volume-title":"Automata, Languages, and Machines","author":"S. Eilenberg","year":"1974","unstructured":"Eilenberg, S.: Automata, Languages, and Machines. ch. 3. Academic Press, London (1974)"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Greve, D.A., Kaufmann, M., et al.: Efficient execution in an automated reasoning environment. Journal of Functional Programming (to appear, 2007)","DOI":"10.1017\/S0956796807006338"},{"key":"14_CR6","unstructured":"Haftmann, F.: Code generation from Isabelle\/HOL theories, available in the Isabelle distribution (2007)"},{"key":"14_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11814771_48","volume-title":"Automated Reasoning","author":"A. Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 589\u2013603. Springer, Heidelberg (2006)"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1145\/1060745.1060809","volume-title":"Proceedings of the 14th International World Wide Web Conference","author":"Y. Minamide","year":"2005","unstructured":"Minamide, Y.: Static approximation of dynamically generated Web pages. In: Proceedings of the 14th International World Wide Web Conference, pp. 432\u2013441. ACM Press, New York (2005)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11924661_22","volume-title":"Programming Languages and Systems","author":"Y. Minamide","year":"2006","unstructured":"Minamide, Y., Tozawa, A.: XML validation for context-free grammars. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol.\u00a04279, pp. 357\u2013373. Springer, Heidelberg (2006)"},{"key":"14_CR10","series-title":"ch. 5","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-1-4757-3188-0_5","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"J. Strother Moore","year":"2000","unstructured":"Strother Moore, J.: An exercise in graph theory. In: Kaufmann, M., Manolios, P., Strother Moore, J. (eds.) Computer-Aided Reasoning: ACL2 Case Studies. ch. 5, pp. 41\u201374. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"14_CR11","unstructured":"Murata, M.: Hedge automata: a formal model for XML schemata (1999), http:\/\/www.xml.gr.jp\/relax\/hedge_nice.html"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055126","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol.\u00a01479, pp. 1\u201315. Springer, Heidelberg (1998)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"6","key":"14_CR14","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1016\/S0019-9958(68)90999-6","volume":"13","author":"C. Pair","year":"1968","unstructured":"Pair, C., Quere, A.: D\u00e9finition et \u00e9tude des bilangages r\u00e9guliers. Information and Control\u00a013(6), 565\u2013593 (1968)","journal-title":"Information and Control"},{"issue":"11\u201312","key":"14_CR15","first-page":"701","volume":"40","author":"T. Reps","year":"2000","unstructured":"Reps, T.: Program analysis via graph reachability. Information and Software Technology\u00a040(11\u201312), 701\u2013726 (2000)","journal-title":"Information and Software Technology"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/3-540-44755-5_25","volume-title":"Theorem Proving in Higher Order Logics","author":"X. Rival","year":"2001","unstructured":"Rival, X., Goubault-Larrecq, J.: Experiments with finite tree automata in Coq. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 362\u2013377. Springer, Heidelberg (2001)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/978-3-540-71389-0_25","volume-title":"Proc. of Tenth International Conference on Foundations of Software Science and Computation Structures","author":"A. Tozawa","year":"2007","unstructured":"Tozawa, A., Minamide, Y.: Complexity results on balanced context-free languages. In: Proc. of Tenth International Conference on Foundations of Software Science and Computation Structures. LNCS, vol.\u00a04423, pp. 346\u2013360. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:28:06Z","timestamp":1619519286000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}