{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T21:17:25Z","timestamp":1769375845434,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2004,9,27]],"date-time":"2004-09-27T00:00:00Z","timestamp":1096243200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2004,9,27]]},"DOI":"10.1145\/1017753.1017794","type":"proceedings-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:39:48Z","timestamp":1097170788000},"page":"249-258","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["A methodology for generating verified combinatorial circuits"],"prefix":"10.1145","author":[{"given":"Oleg","family":"Kiselyov","sequence":"first","affiliation":[{"name":"Fleet Numerical Meteorology and Oceanography Center, Monterey, CA"}]},{"given":"Kedar N.","family":"Swadi","sequence":"additional","affiliation":[{"name":"Rice University"}]},{"given":"Walid","family":"Taha","sequence":"additional","affiliation":[{"name":"Rice University"}]}],"member":"320","published-online":{"date-parts":[[2004,9,27]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Structure and Interpretation of Computer Programs","author":"Abelson H.","year":"1996","unstructured":"H. Abelson , G.J. Sussman , and J. Sussman . Structure and Interpretation of Computer Programs . The MIT Press (Cambridge, MA ) and McGraw-Hill Book Company (New York , NY), 1996 . Available online from http:\/\/mitpress.mit.edu\/sicp\/full-text\/book\/book.html.]] H. Abelson, G.J. Sussman, and J. Sussman. Structure and Interpretation of Computer Programs. The MIT Press (Cambridge, MA) and McGraw-Hill Book Company (New York, NY), 1996. Available online from http:\/\/mitpress.mit.edu\/sicp\/full-text\/book\/book.html.]]"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289440"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1013623303037"},{"key":"e_1_3_2_1_4_1","series-title":"Lecture Notes in Computer Science","volume-title":"Generative Programming and Component Engineering (GPCE)","author":"Calcagno Cristiano","year":"2003","unstructured":"Cristiano Calcagno , Walid Taha , Liwen Huang , and Xavier Leroy . Implementing multi-stage languages using ASTs, gensym, and reflection . In Krzysztof Czarnecki, Frank Pfenning, and Yannis Smaragdakis, editors, Generative Programming and Component Engineering (GPCE) , Lecture Notes in Computer Science . Springer-Verlag , 2003 .]] Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy. Implementing multi-stage languages using ASTs, gensym, and reflection. In Krzysztof Czarnecki, Frank Pfenning, and Yannis Smaragdakis, editors, Generative Programming and Component Engineering (GPCE), Lecture Notes in Computer Science. Springer-Verlag, 2003.]]"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.839320"},{"key":"e_1_3_2_1_7_1","volume-title":"July","author":"Eckhardt Jason","year":"2004","unstructured":"Jason Eckhardt , Roumen Kaiabachev , Oleg Kiselyov , Kedar N. Swadi , and Walid Taha . Monadic multi-stage programming. In preparation , July 2004 .]] Jason Eckhardt, Roumen Kaiabachev, Oleg Kiselyov, Kedar N. Swadi, and Walid Taha. Monadic multi-stage programming. In preparation, July 2004.]]"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301661"},{"key":"e_1_3_2_1_9_1","volume-title":"Fifth International Workshop on Designing Correct Circuits","author":"Grundy Jim","year":"2004","unstructured":"Jim Grundy , Tom Melham , and John O'Leary . A reflective functional language for hardware design and theorem proving . In Fifth International Workshop on Designing Correct Circuits , March 2004 .]] Jim Grundy, Tom Melham, and John O'Leary. A reflective functional language for hardware design and theorem proving. In Fifth International Workshop on Designing Correct Circuits, March 2004.]]"},{"key":"e_1_3_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"European Symposium on Programming (ESOP)","author":"Hofmann Martin","year":"2000","unstructured":"Martin Hofmann . A type system for bounded space and functional in-place update . In European Symposium on Programming (ESOP) , Lecture Notes in Computer Science . Springer-Verlag , 2000 .]] Martin Hofmann. A type system for bounded space and functional in-place update. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer-Verlag, 2000.]]"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/78.482008"},{"key":"e_1_3_2_1_12_1","series-title":"Lecture Notes in Computer Science","volume-title":"Mathematics of Program Construction","author":"Jones Geraint","year":"1993","unstructured":"Geraint Jones and Mary Sheeran . Designing arithmetic circuits by refinement in ruby . In C. C. Morgan R. S. Bird and J. C. P. Woodcock, editors, Mathematics of Program Construction , Lecture Notes in Computer Science . Springer Verlag , 1993 .]] Geraint Jones and Mary Sheeran. Designing arithmetic circuits by refinement in ruby. In C. C. Morgan R. S. Bird and J. C. P. Woodcock, editors, Mathematics of Program Construction, Lecture Notes in Computer Science. Springer Verlag, 1993.]]"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317784"},{"key":"e_1_3_2_1_15_1","unstructured":"Xavier Leroy. Objective Caml 2000. Available from http:\/\/caml.inria.fr\/ocaml\/.]]  Xavier Leroy. Objective Caml 2000. Available from http:\/\/caml.inria.fr\/ocaml\/.]]"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.1986.294900"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.642810"},{"key":"e_1_3_2_1_18_1","volume-title":"Fifth International Workshop on Designing Correct Circuits","author":"Martin Andrew K.","year":"2004","unstructured":"Andrew K. Martin . HML : A language for high-level design of high-frequency circuits . In Fifth International Workshop on Designing Correct Circuits , March 2004 .]] Andrew K. Martin. HML: A language for high-level design of high-frequency circuits. In Fifth International Workshop on Designing Correct Circuits, March 2004.]]"},{"key":"e_1_3_2_1_19_1","volume-title":"FPL '98","author":"McKay Nicholas","year":"1998","unstructured":"Nicholas McKay and Satnam Singh . Dynamic specialisation of XC6200 FPGAs by partial evaluation. In Field-Programmable Logic and Applications. From FPGAs to Computing Paradigm: 8th International Workshop , FPL '98 , Tallinn, Estonia , August 1998 .]] Nicholas McKay and Satnam Singh. Dynamic specialisation of XC6200 FPGAs by partial evaluation. In Field-Programmable Logic and Applications. From FPGAs to Computing Paradigm: 8th International Workshop, FPL '98, Tallinn, Estonia, August 1998.]]"},{"key":"e_1_3_2_1_20_1","volume-title":"A compiled, type-safe multi-stage programming language. Available online from http:\/\/www.metaocaml.org\/","year":"2003","unstructured":"MetaOCaml : A compiled, type-safe multi-stage programming language. Available online from http:\/\/www.metaocaml.org\/ , 2003 .]] MetaOCaml: A compiled, type-safe multi-stage programming language. Available online from http:\/\/www.metaocaml.org\/, 2003.]]"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1220583"},{"key":"e_1_3_2_1_23_1","volume-title":"Fifth International Workshop on Designing Correct Circuits","author":"O'Donnell John","year":"2004","unstructured":"John O'Donnell . Integrating formal methods with digital circuit design in Hydra . In Fifth International Workshop on Designing Correct Circuits , March 2004 .]] John O'Donnell. Integrating formal methods with digital circuit design in Hydra. In Fifth International Workshop on Designing Correct Circuits, March 2004.]]"},{"key":"e_1_3_2_1_24_1","first-page":"97291","volume":"91000","author":"Oregon Graduate Institute Technical Reports. P.O","unstructured":"Oregon Graduate Institute Technical Reports. P.O . Box 91000 , Portland, OR 97291 - 91000 ,USA. Available online from ftp:\/\/cse.ogi.edu\/pub\/tech-reports\/README.html.]] Oregon Graduate Institute Technical Reports. P.O. Box 91000, Portland, OR 97291-1000,USA. Available online from ftp:\/\/cse.ogi.edu\/pub\/tech-reports\/README.html.]]","journal-title":"Box"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581499"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/646705.702180"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/328690.328697"},{"key":"e_1_3_2_1_29_1","series-title":"Lecture Notes in Computer Science","volume-title":"Domain-specific Program Generation","author":"Taha Walid","year":"2004","unstructured":"Walid Taha . A gentle introduction to multi-stage programming . In Don Batory, Charles Consel, Christian Lengauer, and Martin Odersky, editors, Domain-specific Program Generation , Lecture Notes in Computer Science . Springer-Verlag , 2004 .]] Walid Taha. A gentle introduction to multi-stage programming. In Don Batory, Charles Consel, Christian Lengauer, and Martin Odersky, editors, Domain-specific Program Generation, Lecture Notes in Computer Science. Springer-Verlag, 2004.]]"},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the Third International Conference on Embedded Software","author":"Taha Walid","year":"2003","unstructured":"Walid Taha , Stephan Ellner , and Hongwei Xi . Generating Imperative, Heap-Bounded Programs in a Functional Setting . In Proceedings of the Third International Conference on Embedded Software , Philadelphia, PA , October 2003 .]] Walid Taha, Stephan Ellner, and Hongwei Xi. Generating Imperative, Heap-Bounded Programs in a Functional Setting. In Proceedings of the Third International Conference on Embedded Software, Philadelphia, PA, October 2003.]]"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604134"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2464-6","volume-title":"The Verilog Hardware Description Language","author":"Thomas Donald E.","year":"1996","unstructured":"Donald E. Thomas and Philip R. Moorby . The Verilog Hardware Description Language . Kluwer Academic Publishers , 3 rd edition, 1996 .]] Donald E. Thomas and Philip R. Moorby. The Verilog Hardware Description Language. Kluwer Academic Publishers, 3rd edition, 1996.]]","edition":"3"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"}],"event":{"name":"EMSOFT04: Fourth ACM International Conference on Embedded Software 2004","location":"Pisa Italy","acronym":"EMSOFT04","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 4th ACM international conference on Embedded software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1017753.1017794","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1017753.1017794","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:36:46Z","timestamp":1750282606000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1017753.1017794"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,9,27]]},"references-count":31,"alternative-id":["10.1145\/1017753.1017794","10.1145\/1017753"],"URL":"https:\/\/doi.org\/10.1145\/1017753.1017794","relation":{},"subject":[],"published":{"date-parts":[[2004,9,27]]},"assertion":[{"value":"2004-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}