{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:03:21Z","timestamp":1742961801884,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005893"},{"type":"electronic","value":"9783642005909"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00590-9_11","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T12:05:58Z","timestamp":1238155558000},"page":"143-159","source":"Crossref","is-referenced-by-count":5,"title":["Formalising and Verifying Reference Attribute Grammars in Coq"],"prefix":"10.1007","author":[{"given":"Max","family":"Sch\u00e4fer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Torbj\u00f6rn","family":"Ekman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oege","family":"de Moor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Augusteijn, L.: Definition of the programming language Elegant, 2000. Release 7.1, Philips Research Laboratories, Eindhoven, the Netherlands (February 2000)","key":"11_CR1"},{"unstructured":"Badouel, \u00c9., Fotsing, B., Tchougong, R.: Yet Another Implementation of Attribute Evaluation. Technical Report 6315, INRIA Rennes (2007)","key":"11_CR2"},{"issue":"4","key":"11_CR3","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1145\/1082036.1082042","volume":"52","author":"J.T. Boyland","year":"2005","unstructured":"Boyland, J.T.: Remote attribute grammars. J. ACM\u00a052(4), 627\u2013687 (2005)","journal-title":"J. ACM"},{"issue":"1","key":"11_CR4","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.tcs.2005.06.004","volume":"342","author":"D. Cachera","year":"2005","unstructured":"Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. Theor. Comput. Sci.\u00a0342(1), 56\u201378 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01744285","volume":"13","author":"L.M. Chirica","year":"1979","unstructured":"Chirica, L.M., Martin, D.F.: An Order-Algebraic Definition of Knuthian Semantics. Mathematical Systems Theory\u00a013, 1\u201327 (1979)","journal-title":"Mathematical Systems Theory"},{"unstructured":"Ekman, T., Ettinger, R., Sch\u00e4fer, M., Verbaere, M.: Refactoring bugs (2008), http:\/\/progtools.comlab.ox.ac.uk\/refactoring\/bugreports","key":"11_CR6"},{"doi-asserted-by":"crossref","unstructured":"Ekman, T., Hedin, G.: The JastAdd Extensible Java Compiler. In: OOPSLA (2007)","key":"11_CR7","DOI":"10.1145\/1297846.1297881"},{"doi-asserted-by":"crossref","unstructured":"Farrow, R.: Automatic generation of fixed-point-finding evaluators for circular, but well-defined, attribute grammars. In: CC, pp. 85\u201398 (1986)","key":"11_CR8","DOI":"10.1145\/12276.13320"},{"unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification (2005)","key":"11_CR9"},{"doi-asserted-by":"crossref","unstructured":"Hanson, D., Proebsting, T.: A research C# compiler. SPE\u00a034(13) (2004)","key":"11_CR10","DOI":"10.1002\/spe.610"},{"unstructured":"Hedin, G.: Reference Attributed Grammars. Informatica\u00a0(24), 301\u2013317 (2000)","key":"11_CR11"},{"issue":"5","key":"11_CR12","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"G.P. Huet","year":"1997","unstructured":"Huet, G.P.: The Zipper. J. Funct. Program.\u00a07(5), 549\u2013554 (1997)","journal-title":"J. Funct. Program."},{"issue":"1","key":"11_CR13","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1006\/inco.2002.3092","volume":"177","author":"A. Igarashi","year":"2002","unstructured":"Igarashi, A., Pierce, B.C.: On inner classes. Inf. and Comp.\u00a0177(1), 56\u201389 (2002)","journal-title":"Inf. and Comp."},{"doi-asserted-by":"crossref","unstructured":"Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: A Minimal Core Calculus for Java and GJ. In: OOPSLA, pp. 132\u2013146 (1999)","key":"11_CR14","DOI":"10.1145\/320385.320395"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-18317-5_10","volume-title":"Functional Programming Languages and Computer Architecture","author":"T. Johnsson","year":"1987","unstructured":"Johnsson, T.: Attribute grammars as a functional programming paradigm. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol.\u00a0274, pp. 154\u2013173. Springer, Heidelberg (1987)"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF01692511","volume":"2","author":"D.E. Knuth","year":"1968","unstructured":"Knuth, D.E.: Semantics of context-free languages. Mathematical Systems Theory\u00a02, 127\u2013146 (1968); correction: Mathematical Systems Theory 5, 95\u201396 (1971)","journal-title":"Mathematical Systems Theory"},{"key":"11_CR17","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1145\/503272.503299","volume-title":"POPL","author":"D. Lacey","year":"2002","unstructured":"Lacey, D., Jones, N.D., Van Wyk, E., Frederiksen, C.C.: Proving Correctness of Compiler Optimizations by Temporal Logic. In: POPL, pp. 283\u2013294. ACM Press, New York (2002)"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1145\/1047659.1040335","volume":"40","author":"S. Lerner","year":"2005","unstructured":"Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. SIGPLAN Not.\u00a040(1), 364\u2013377 (2005)","journal-title":"SIGPLAN Not."},{"doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end. In: POPL, pp. 42\u201354 (2006)","key":"11_CR19","DOI":"10.1145\/1111037.1111042"},{"issue":"1","key":"11_CR20","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.scico.2005.06.005","volume":"68","author":"E. Magnusson","year":"2007","unstructured":"Magnusson, E., Hedin, G.: Circular Reference Attributed Grammars. Sci. Comput. Program.\u00a068(1), 21\u201337 (2007)","journal-title":"Sci. Comput. Program."},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-48737-9_4","volume-title":"Formal Syntax and Semantics of Java","author":"D. Oheimb von","year":"1999","unstructured":"von Oheimb, D., Nipkow, T.: Machine-checking the java specification: Proving type-safety. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523, p. 119. Springer, Heidelberg (1999)"},{"issue":"1","key":"11_CR22","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/200994.201001","volume":"17","author":"J. Palsberg","year":"1995","unstructured":"Palsberg, J.: Closure Analysis in Constraint Form. TOPLAS\u00a017(1), 47\u201362 (1995)","journal-title":"TOPLAS"},{"key":"11_CR23","volume-title":"Texts and Monographs in Computer Science","author":"T.W. Reps","year":"1989","unstructured":"Reps, T.W., Teitelbaum, T.: The Synthesizer Generator: A system for constructing language-based editors. In: Texts and Monographs in Computer Science. Springer, Heidelberg (1989)"},{"key":"11_CR24","volume-title":"OOPSLA","author":"M. Sch\u00e4fer","year":"2008","unstructured":"Sch\u00e4fer, M., Ekman, T., de Moor, O.: Sound and Extensible Renaming for Java. In: Kiczales, G. (ed.) OOPSLA. ACM Press, New York (2008)"},{"doi-asserted-by":"crossref","unstructured":"Sch\u00e4fer, M., Ekman, T., de Moor, O.: Formalising and Verifying Reference Attribute Grammars in Coq (Technical Report and Implementation) (2009), http:\/\/progtools.comlab.ox.ac.uk\/projects\/refactoring\/formalising-rags","key":"11_CR25","DOI":"10.1007\/978-3-642-00590-9_11"},{"unstructured":"Sestoft, P.: Analysis and Efficient Implementation of Funct. Prog. Ph.D. thesis (1991)","key":"11_CR26"},{"doi-asserted-by":"crossref","unstructured":"Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strnisa, R.: Ott: effective tool support for the working semanticist. In: ICFP, pp. 1\u201312 (2007)","key":"11_CR27","DOI":"10.1145\/1291151.1291155"},{"unstructured":"Ekman, T.: JastAdd (2008), http:\/\/www.jastadd.org","key":"11_CR28"},{"unstructured":"Uustalu, T., Vene, V.: Comonadic functional attribute evaluation. In: TFP (2005)","key":"11_CR29"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00590-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T17:08:35Z","timestamp":1684948115000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00590-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005893","9783642005909"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00590-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}