{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T22:22:47Z","timestamp":1648938167893},"reference-count":10,"publisher":"Elsevier BV","issue":"5","license":[{"start":{"date-parts":[[2011,3,1]],"date-time":"2011-03-01T00:00:00Z","timestamp":1298937600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":881,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2011,3]]},"DOI":"10.1016\/j.entcs.2011.02.019","type":"journal-article","created":{"date-parts":[[2011,3,7]],"date-time":"2011-03-07T15:16:19Z","timestamp":1299510979000},"page":"119-134","source":"Crossref","is-referenced-by-count":1,"title":["Simulating Finite Eilenberg Machines with a Reactive Engine"],"prefix":"10.1016","volume":"229","author":[{"given":"Beno\u00eet","family":"Razet","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2011.02.019_br0010","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","article-title":"Interactive Theorem Proving and Program Development: Coq\u02bcArt, the Calculus of Inductive Constructions","author":"Bertot","year":"2004"},{"key":"10.1016\/j.entcs.2011.02.019_br0020","unstructured":"The Coq team, The Coq proof assistant, software and documentation, 1995\u20132008. Available at http:\/\/coq.inria.fr\/."},{"issue":"8","key":"10.1016\/j.entcs.2011.02.019_br0030","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","article-title":"Proving termination with multiset orderings","volume":"22","author":"Dershowitz","year":"1979","journal-title":"Commun. of ACM"},{"key":"10.1016\/j.entcs.2011.02.019_br0040","series-title":"Automata, Languages, and Machines, Volume A","author":"Eilenberg","year":"1974"},{"issue":"4","key":"10.1016\/j.entcs.2011.02.019_br0050","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1017\/S0956796804005416","article-title":"A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger","volume":"15","author":"Huet","year":"2005","journal-title":"J. of Funct. Program."},{"key":"10.1016\/j.entcs.2011.02.019_br0060","series-title":"Algebra, Meaning and Computation: Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday","first-page":"355","article-title":"The reactive engine for modular transducers","volume":"4060","author":"Huet","year":"2006"},{"key":"10.1016\/j.entcs.2011.02.019_br0070","unstructured":"Leroy, X., D. Doligez, J. Garrigue and J. Vouillon, The Objective Caml system, software and documentation, 1996\u20132006. Available at http:\/\/caml.inria.fr\/."},{"key":"10.1016\/j.entcs.2011.02.019_br0080","series-title":"Proc. of 13th Int. Conf. on Implementation and Application of Automata","first-page":"242","article-title":"Finite Eilenberg machines","volume":"5148","author":"Razet","year":"2008"},{"key":"10.1016\/j.entcs.2011.02.019_br0090","unstructured":"Razet, B., Simulating Eilenberg machines with a reactive engine: formal specification, proof and program extraction, Research Report No. 6487, INRIA, 2008. Available at https:\/\/hal.inria.fr\/inria-00257352."},{"key":"10.1016\/j.entcs.2011.02.019_br0100","series-title":"Revised Selected Papers from Int. Wksh. on Types for Proofs and Programs","first-page":"237","article-title":"Subset coercions in Coq","volume":"4502","author":"Sozeau","year":"2007"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066111000569?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066111000569?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,12,4]],"date-time":"2018-12-04T01:52:25Z","timestamp":1543888345000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066111000569"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3]]},"references-count":10,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2011,3]]}},"alternative-id":["S1571066111000569"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2011.02.019","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2011,3]]}}}