{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:39:50Z","timestamp":1770277190009,"version":"3.49.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319071503","type":"print"},{"value":"9783319071510","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-07151-0_14","type":"book-chapter","created":{"date-parts":[[2014,5,21]],"date-time":"2014-05-21T23:30:14Z","timestamp":1400715014000},"page":"221-237","source":"Crossref","is-referenced-by-count":4,"title":["Proving Correctness of Compilers Using Structured Graphs"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Bahr","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Ager, M.S., Biernacki, D., Danvy, O., Midtgaard, J.: From interpreter to compiler and virtual machine: A functional derivation. Tech. Rep. RS-03-14, BRICS, Department of Computer Science, University of Aarhus (2003)","DOI":"10.7146\/brics.v10i14.21784"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Bahr, P.: Proving correctness of compilers using structured graphs (extended version). Tech. rep., University of Copenhagen (2014)","DOI":"10.1007\/978-3-319-07151-0_14"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Bahr, P., Hutton, G.: Calculating correct compilers (2014) (unpublished manuscript)","DOI":"10.1017\/S0956796815000180"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bernardy, J.P., Pouillard, N.: Names for free: polymorphic views of names and binders. In: Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, pp. 13\u201324. ACM (2013)","DOI":"10.1145\/2503778.2503780"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, pp. 143\u2013156. ACM (2008)","DOI":"10.1145\/1411204.1411226"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: A verified compiler for an impure functional language. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 93\u2013106. ACM (2010)","DOI":"10.1145\/1706299.1706312"},{"issue":"6","key":"14_CR7","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"M.A. Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes\u00a028(6), 2 (2003)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Gill, A., Launchbury, J., Peyton Jones, S.L.: A short cut to deforestation. In: Proceedings of the Conference on Functional Programming Languages and Computer Architecture, pp. 223\u2013232. ACM (1993)","DOI":"10.1145\/165180.165214"},{"key":"14_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813672","volume-title":"Programming in Haskell","author":"G. Hutton","year":"2007","unstructured":"Hutton, G.: Programming in Haskell, vol.\u00a02. Cambridge University Press, Cambridge (2007)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-27764-4_12","volume-title":"Mathematics of Program Construction","author":"G. Hutton","year":"2004","unstructured":"Hutton, G., Wright, J.: Compiling exceptions correctly. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, pp. 211\u2013227. Springer, Heidelberg (2004)"},{"issue":"6","key":"14_CR11","doi-asserted-by":"crossref","first-page":"777","DOI":"10.1017\/S0956796807006363","volume":"17","author":"G. Hutton","year":"2007","unstructured":"Hutton, G., Wright, J.: What is the meaning of these constant interruptions? J. Funct. Program.\u00a017(6), 777\u2013792 (2007)","journal-title":"Funct. Program."},{"issue":"4","key":"14_CR12","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1023\/A:1022982420888","volume":"15","author":"P. Johann","year":"2002","unstructured":"Johann, P.: A generalization of short-cut fusion and its correctness proof. Higher Order Symbol. Comput.\u00a015(4), 273\u2013300 (2002)","journal-title":"Higher Order Symbol. Comput."},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 42\u201354. ACM (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"14_CR14","unstructured":"Marlow, S.: Haskell 2010 language report (2010)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Matsuda, K., Inaba, K., Nakano, K.: Polynomial-time inverse computation for accumulative functions with multiple data traversals. In: Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, pp. 5\u201314. ACM (2012)","DOI":"10.1145\/2103746.2103752"},{"key":"14_CR16","unstructured":"Meijer, E.: Calculating Compilers. Ph.D. thesis, Katholieke Universiteit Nijmegen (1992)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Oliveira, B.C.D.S., L\u00f6h, A.: Abstract syntax graphs for domain specific languages. In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, pp. 87\u201396. ACM (2013)","DOI":"10.1145\/2426890.2426909"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Oliveira, B.C., Cook, W.R.: Functional programming with structured graphs. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, pp. 77\u201388. ACM (2012)","DOI":"10.1145\/2364527.2364541"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Ramsey, N., Dias, J.A., Peyton Jones, S.: Hoopl: a modular, reusable library for dataflow analysis and transformation. In: Proceedings of the Third ACM Haskell Symposium on Haskell, pp. 121\u2013134. ACM (2010)","DOI":"10.1145\/2088456.1863539"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Ramsey, N., Dias, J.: An applicative control-flow graph based on huet\u2019s zipper. In: Proceedings of the ACM-SIGPLAN Workshop on ML, pp. 105\u2013126 (2006)","DOI":"10.1016\/j.entcs.2005.11.042"},{"issue":"3","key":"14_CR21","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1145\/357172.357179","volume":"4","author":"M. Wand","year":"1982","unstructured":"Wand, M.: Deriving target code as a representation of continuation semantics. ACM Trans. Program. Lang. Syst.\u00a04(3), 496\u2013517 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07151-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T18:15:38Z","timestamp":1558894538000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-07151-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319071503","9783319071510"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07151-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}