{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:54Z","timestamp":1725467514670},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055126","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"1-15","source":"Crossref","is-referenced-by-count":19,"title":["Verified lexical analysis"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"1_CR1","unstructured":"R. Bird and P. Wadler. Introduction to Functional Programming. Prentice-Hall, 1988."},{"key":"1_CR2","unstructured":"R. Constable, P. Jackson, P. Naumov, and J. Uribe. Constructively formalizing automata. In G. Plotkin and M. Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1998. To appear."},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"W. Feischer. Berechenbarheit. Springer-Verlag, 1993.","DOI":"10.1007\/978-3-642-78019-6"},{"key":"1_CR4","unstructured":"J.-C. Filli\u00e2tre. Finite automata theory in Coq. A constructive proof of Kleene's theorem. Technical Report 97-04, Laboratoire de l'Informatique du Parall\u00e9lisme, Ecole Normale Sup\u00e9rieure de Lyon, 1997."},{"key":"1_CR5","unstructured":"R. Handl. Verifikation eines Scanners (mit Isabelle). Master's thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1993."},{"key":"1_CR6","unstructured":"J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979."},{"key":"1_CR7","unstructured":"C. Kreitz. Constructive automata theory implemented with the Nuprl proof development system. Technical Report TR 86-779, Dept. of Computer Science, Cornell University, 1986."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1180 of Lect. Notes in Comp. Sci., pages 180\u2013192. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-62034-6_48"},{"key":"1_CR9","unstructured":"L. C. Paulson. Generic automatic proof tools. In R. Veroff, editor, Automated Reasoning and its Applications. MIT Press, 1997. Also Report 396, Computer Laboratory, University of Cambridge."},{"key":"1_CR10","unstructured":"L. C. Paulson. A generic tableau prover and its integration with Isabelle. Technical Report 441, University of Cambridge, Computer Laboratory, 1998."},{"key":"1_CR11","unstructured":"S. Thompson. Regular expressions and automata using Miranda. Available at http:\/\/www.cs.ukc.ac.uk\/pubs\/1995\/212, 1995."}],"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\/BFb0055126","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T04:34:06Z","timestamp":1555734846000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055126"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0055126","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}