{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T20:35:18Z","timestamp":1768163718465,"version":"3.49.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2001,12,1]],"date-time":"2001-12-01T00:00:00Z","timestamp":1007164800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,12,1]],"date-time":"2001-12-01T00:00:00Z","timestamp":1007164800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order and Symbolic Computation"],"published-print":{"date-parts":[[2001,12]]},"DOI":"10.1023\/a:1014408032446","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T20:35:40Z","timestamp":1041107740000},"page":"387-409","source":"Crossref","is-referenced-by-count":15,"title":["From Syntactic Theories to Interpreters: Automating the Proof of Unique Decomposition"],"prefix":"10.1007","volume":"14","author":[{"given":"Yong","family":"Xiao","sequence":"first","affiliation":[]},{"given":"Amr","family":"Sabry","sequence":"additional","affiliation":[]},{"given":"Zena M.","family":"Ariola","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"397963_CR1","volume-title":"Compilers-Principles, Techniques, and Tools","author":"A. Aho","year":"1985","unstructured":"Aho, A., Sethi, R., and Ullman, J. Compilers-Principles, Techniques, and Tools. Addison-Wesley, Reading, MA, 1985."},{"issue":"3","key":"397963_CR2","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1017\/S0956796897002724","volume":"7","author":"Z.M. Ariola","year":"1997","unstructured":"Ariola, Z.M. and Felleisen, M. The call-by-need lambda calculus. J. Functional Programming, 7(3) (1997) 265-301.","journal-title":"J. Functional Programming"},{"key":"397963_CR3","series-title":"Vol. 103 of Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics, Vol. 103 of Studies in Logic and the Foundations of Mathematics. Elsevier Science Publishers B.V., Amsterdam, 1984."},{"key":"397963_CR4","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemart, F., Lugiez, D., Tison, S., and Tommasi, M. Tree Automata Techniques and Applications, 1999. Book draft available at http:\/\/www.grappa.univ-lille3.fr\/tata."},{"key":"397963_CR5","doi-asserted-by":"crossref","unstructured":"de Bruijn, N. The mathematical language AUTOMATH, its usage, and some of its extensions. In Proceedings of the Symposium on Automatic Demonstration. Versailles, France, M. Laudet (Ed.). LNM, Vol. 125, Springer-Verlag, 1968, pp. 29-61.","DOI":"10.1007\/BFb0060623"},{"key":"397963_CR6","unstructured":"Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C., and Werner, B. The Coq proof assistant user's guide. Technical Report Rapport Techniques 154, INRIA, Rocquencourt, France, 1993. Version 5.8."},{"key":"397963_CR7","first-page":"75","volume-title":"ACM SIGPLAN International Conference on Functional Programming","author":"M. F\u00e4hndrich","year":"1997","unstructured":"F\u00e4hndrich, M. and Boyland, J. Statically checkable pattern abstractions. In ACM SIGPLAN International Conference on Functional Programming. ACM Press, New York, 1997, pp. 75-84."},{"key":"397963_CR8","unstructured":"Felleisen, M. The calculi of lambda-v-CS-conversion: A syntactic theory of control and state in imperative higher-order programming languages. Ph.D. Thesis, Indiana University, 1987."},{"key":"397963_CR9","doi-asserted-by":"crossref","unstructured":"Fiskio-Lasseter, J. and Sabry, A. Putting operational techniques to the test: A syntactic theory for behavioral Verilog. In Electronic Notes in Theoretical Computer Science, Vol. 26, 1999, pp. 32-49. Also in Third International Workshop on Higher Order Operational Techniques in Semantics.","DOI":"10.1016\/S1571-0661(05)80282-8"},{"key":"397963_CR10","volume-title":"Tree Automata","author":"F. G\u00e9cseg","year":"1984","unstructured":"G\u00e9cseg, F. and Steinby, M. Tree Automata. Budapest, Akad\u00e9miai Kiad\u00f3 , 1984."},{"key":"397963_CR11","volume-title":"Introduction toAutomata Theory, Languages, and Computation, Computer Science","author":"J. Hopcroft","year":"1979","unstructured":"Hopcroft, J. and Ullman, J. Introduction toAutomata Theory, Languages, and Computation, Computer Science. Addison-Wesley, Reading, MA, 1979."},{"key":"397963_CR12","first-page":"227","volume-title":"ACM SIGPLAN International Conference on Functional Programming","author":"J. Launchbury","year":"1997","unstructured":"Launchbury, J. and Sabry, A. Monadic state: Axiomatization and type safety. In ACM SIGPLAN International Conference on Functional Programming. ACM Press, New York, 1997, pp. 227-238."},{"issue":"2","key":"397963_CR13","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1010052222987","volume":"12","author":"I.A. Mason","year":"1999","unstructured":"Mason, I.A. Computing with contexts. Higher-Order and Symbolic Computation, 12(2) (1999) 171-201.","journal-title":"Higher-Order and Symbolic Computation"},{"key":"397963_CR14","first-page":"202","volume-title":"Proceedings of the 16th International Conference on Automated Deduction. Trento, Italy","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F. and Sch\u00fcrmann, C. System description: Twelf-a meta-logical framework for deductive systems. In Proceedings of the 16th International Conference on Automated Deduction. Trento, Italy, H. Ganzinger (Ed.). Springer-Verlag, Berlin, 1999, pp. 202-206."},{"key":"397963_CR15","first-page":"8","volume-title":"ACM SIGPLAN International Conference on Functional Programming","author":"M. Semmelroth","year":"1999","unstructured":"Semmelroth, M. and Sabry, A. Monadic encapsulation in ML. In ACM SIGPLAN International Conference on Functional Programming. ACM Press, New York, 1999, pp. 8-17."},{"key":"397963_CR16","unstructured":"Xiao, Y., Ariola, Z.M., and Mauny, M. From syntactic theories to interpreters: A specification language and its compiler. In Proceedings of the First International Workshop on Rule-based Programming. Montr\u00e9al, Canada, N. Derschowitz and C. Kirchner (Eds.). 2000, pp. 1-16. The proceedings are also available at http:\/\/www.loria.fr\/~ckirchne\/=rule2000\/proceedings\/."}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1014408032446.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1014408032446\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1014408032446.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:56:13Z","timestamp":1751982973000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1014408032446"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,12]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2001,12]]}},"alternative-id":["397963"],"URL":"https:\/\/doi.org\/10.1023\/a:1014408032446","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,12]]}}}