{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:20:02Z","timestamp":1750220402125,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":65,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,9,6]],"date-time":"2021-09-06T00:00:00Z","timestamp":1630886400000},"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":[[2021,9,6]]},"DOI":"10.1145\/3479394.3479417","type":"proceedings-article","created":{"date-parts":[[2021,10,7]],"date-time":"2021-10-07T22:23:02Z","timestamp":1633645382000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Mechanized Semantic Metalanguage for High Level Synthesis"],"prefix":"10.1145","author":[{"given":"William L.","family":"Harrison","sequence":"first","affiliation":[{"name":"Two Six Technologies, USA"}]},{"given":"Chris","family":"Hathhorn","sequence":"additional","affiliation":[{"name":"Cyber Security Research Group, Oak Ridge National Laboratory, USA"}]},{"given":"Gerard","family":"Allwein","sequence":"additional","affiliation":[{"name":"US Naval Research Laboratory, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 40th POPL. 27\u201338","author":"Abel Andreas","year":"2013","unstructured":"Andreas Abel , Brigitte Pientka , David Thibodeau , and Anton Setzer . 2013 . Copatterns: Programming Infinite Structures by Observations . In Proceedings of the 40th POPL. 27\u201338 . Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: Programming Infinite Structures by Observations. In Proceedings of the 40th POPL. 27\u201338."},{"key":"e_1_3_2_1_2_1","unstructured":"David Andrews. 2015. Will the Future Success of Reconfigurable Computing Require a Paradigm Shift in Our Research Community\u2019s Thinking?Keynote address Applied Reconfigurable Computing.  David Andrews. 2015. Will the Future Success of Reconfigurable Computing Require a Paradigm Shift in Our Research Community\u2019s Thinking?Keynote address Applied Reconfigurable Computing."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"C. Baaij and J. Kuper. 2014. Using Rewriting to Synthesize Functional Languages to Digital Circuits. In Trends in Fun. Prog.(LNCS Vol.\u00a08322). 17\u201333.  C. Baaij and J. Kuper. 2014. Using Rewriting to Synthesize Functional Languages to Digital Circuits. In Trends in Fun. Prog.(LNCS Vol.\u00a08322). 17\u201333.","DOI":"10.1007\/978-3-642-45340-3_2"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Jonathan Bachrach Huy Vo Brian Richards Yunsup Lee Andrew Waterman Rimas Avizienis John Wawrzynek and Krste Asanovic. 2012. Chisel: constructing hardware in a Scala embedded language. In DAC. 1216\u20131225.  Jonathan Bachrach Huy Vo Brian Richards Yunsup Lee Andrew Waterman Rimas Avizienis John Wawrzynek and Krste Asanovic. 2012. Chisel: constructing hardware in a Scala embedded language. In DAC. 1216\u20131225.","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_3_2_1_5_1","volume-title":"CHARME","author":"Berry Gerard","year":"2001","unstructured":"Gerard Berry and Ellen Sentovich . 2001 . Multiclock Esterel. In Correct Hardware Design and Verification Methods , CHARME 2001, Vol.\u00a0Lecture Notes in Computer Science, vol 2144. Springer. Gerard Berry and Ellen Sentovich. 2001. Multiclock Esterel. In Correct Hardware Design and Verification Methods, CHARME 2001, Vol.\u00a0Lecture Notes in Computer Science, vol 2144. Springer."},{"key":"e_1_3_2_1_6_1","volume-title":"Lava: Hardware Design in Haskell. In ICFP \u201998. 174\u2013184.","author":"Bjesse Per","year":"1998","unstructured":"Per Bjesse , Koen Claessen , and Mary Sheeran . 1998 . Lava: Hardware Design in Haskell. In ICFP \u201998. 174\u2013184. Per Bjesse, Koen Claessen, and Mary Sheeran. 1998. Lava: Hardware Design in Haskell. In ICFP \u201998. 174\u2013184."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385965"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062358"},{"key":"e_1_3_2_1_9_1","volume-title":"Proc. ACM Program. Lang. 4, POPL, Article 44 (Dec.","author":"Bourke Timothy","year":"2019","unstructured":"Timothy Bourke , L\u00e9lio Brun , and Marc Pouzet . 2019 . Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset . Proc. ACM Program. Lang. 4, POPL, Article 44 (Dec. 2019), 29\u00a0pages. https:\/\/doi.org\/10.1145\/3371112 10.1145\/3371112 Timothy Bourke, L\u00e9lio Brun, and Marc Pouzet. 2019. Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset. Proc. ACM Program. Lang. 4, POPL, Article 44 (Dec. 2019), 29\u00a0pages. https:\/\/doi.org\/10.1145\/3371112"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Ana Bove Peter Dybjer and Ulf Norell. 2009. A Brief Overview of Agda \u2013 A Functional Language with Dependent Types Vol.\u00a05674. 73\u201378.  Ana Bove Peter Dybjer and Ulf Norell. 2009. A Brief Overview of Agda \u2013 A Functional Language with Dependent Types Vol.\u00a05674. 73\u201378.","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_1_11_1","volume-title":"Coquet: A Coq Library for Verifying Hardware. In Certified Programs and Proofs. 330\u2013345.","author":"Braibant Thomas","year":"2011","unstructured":"Thomas Braibant . 2011 . Coquet: A Coq Library for Verifying Hardware. In Certified Programs and Proofs. 330\u2013345. Thomas Braibant. 2011. Coquet: A Coq Library for Verifying Hardware. In Certified Programs and Proofs. 330\u2013345."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"T. Braibant and A. Chlipala. 2013. Formal Verification of Hardware Synthesis. In CAV. 213\u2013228.  T. Braibant and A. Chlipala. 2013. Formal Verification of Hardware Synthesis. In CAV. 213\u2013228.","DOI":"10.1007\/978-3-642-39799-8_14"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2514740"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPT.2013.6718365"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Joonwon Choi Muralidaran Vijayaraghavan Benjamin Sherman Adam Chlipala and Arvind. 2017. Kami: a platform for high-level parametric hardware specification and its modular verification. PACMPL 1(2017) 24:1\u201324:30.  Joonwon Choi Muralidaran Vijayaraghavan Benjamin Sherman Adam Chlipala and Arvind. 2017. Kami: a platform for high-level parametric hardware specification and its modular verification. PACMPL 1(2017) 24:1\u201324:30.","DOI":"10.1145\/3110268"},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings 12th TPHOLs. 91\u2013108","author":"Coupet-Grimal Solange","year":"1999","unstructured":"Solange Coupet-Grimal and Line Jakubiec . 1999 . Hardware Verification Using Co-induction in Coq . In Proceedings 12th TPHOLs. 91\u2013108 . Solange Coupet-Grimal and Line Jakubiec. 1999. Hardware Verification Using Co-induction in Coq. In Proceedings 12th TPHOLs. 91\u2013108."},{"key":"e_1_3_2_1_17_1","first-page":"4","article-title":"Certifying Circuits in Type Theory","volume":"16","author":"Coupet-Grimal Solange","year":"2004","unstructured":"Solange Coupet-Grimal and Line Jakubiec . 2004 . Certifying Circuits in Type Theory . Form. Asp. Comput. 16 , 4 (Nov. 2004), 352\u2013373. Solange Coupet-Grimal and Line Jakubiec. 2004. Certifying Circuits in Type Theory. Form. Asp. Comput. 16, 4 (Nov. 2004), 352\u2013373.","journal-title":"Form. Asp. Comput."},{"volume-title":"Proc. MEMOCODE. 139\u2013148","author":"Czeck E.","key":"e_1_3_2_1_18_1","unstructured":"E. Czeck , R. Nanavati , and J. Stoy . 2006. Reliable Design with Multiple Clock Domains . In Proc. MEMOCODE. 139\u2013148 . E. Czeck, R. Nanavati, and J. Stoy. 2006. Reliable Design with Multiple Clock Domains. In Proc. MEMOCODE. 139\u2013148."},{"key":"e_1_3_2_1_19_1","volume-title":"Fuzzing High-Level Synthesis Tools. In The 2021 ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays","author":"Du Zewei","year":"2021","unstructured":"Zewei Du , Yann Herklotz , Nadesh Ramanathan , and John Wickerson . 2021 . Fuzzing High-Level Synthesis Tools. In The 2021 ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays ( Virtual Event, USA) (FPGA \u201921). Association for Computing Machinery, New York, NY, USA, 148. https:\/\/doi.org\/10.1145\/343 1920.3439466 10.1145\/3431920.3439466 Zewei Du, Yann Herklotz, Nadesh Ramanathan, and John Wickerson. 2021. Fuzzing High-Level Synthesis Tools. In The 2021 ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays (Virtual Event, USA) (FPGA \u201921). Association for Computing Machinery, New York, NY, USA, 148. https:\/\/doi.org\/10.1145\/3431920.3439466"},{"key":"e_1_3_2_1_20_1","first-page":"2006","article-title":"The Challenges of Synthesizing Hardware from C-Like Languages","volume":"23","author":"Edwards A.","year":"2006","unstructured":"Stephen\u00a0 A. Edwards . 2006 . The Challenges of Synthesizing Hardware from C-Like Languages . IEEE Design & Test 23 (2006), 2006 . Stephen\u00a0A. Edwards. 2006. The Challenges of Synthesizing Hardware from C-Like Languages. IEEE Design & Test 23(2006), 2006.","journal-title":"IEEE Design & Test"},{"key":"e_1_3_2_1_23_1","volume-title":"Proc. TYPES.","author":"Paulo\u00a0Pizani Flor Jo\u00e3o","year":"2015","unstructured":"Jo\u00e3o Paulo\u00a0Pizani Flor , Wouter Swierstra , and Yorick Sijsling . 2015 . \u03a0-Ware: Hardware Description and Verification in Agda . In Proc. TYPES. Jo\u00e3o Paulo\u00a0Pizani Flor, Wouter Swierstra, and Yorick Sijsling. 2015. \u03a0-Ware: Hardware Description and Verification in Agda. In Proc. TYPES."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2011.69"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"D. Ghica and A. Jung. 2016. Categorical semantics of digital circuits. In FMCAD.  D. Ghica and A. Jung. 2016. Categorical semantics of digital circuits. In FMCAD.","DOI":"10.1109\/FMCAD.2016.7886659"},{"volume-title":"Field-Programmable Custom Computing Machines, 2000 IEEE Symposium on. 49\u201356","author":"Gokhale M.","key":"e_1_3_2_1_26_1","unstructured":"M. Gokhale , J. Stone , J. Arnold , and M. Kalinowski . 2000. Stream-oriented FPGA computing in the Streams-C high level language . In Field-Programmable Custom Computing Machines, 2000 IEEE Symposium on. 49\u201356 . M. Gokhale, J. Stone, J. Arnold, and M. Kalinowski. 2000. Stream-oriented FPGA computing in the Streams-C high level language. In Field-Programmable Custom Computing Machines, 2000 IEEE Symposium on. 49\u201356."},{"key":"e_1_3_2_1_27_1","volume-title":"Proc. of 10th Annual IEEE LICS(1995)","author":"Gordon Michael","year":"1995","unstructured":"Michael J.\u00a0C. Gordon . 1995 . The semantic challenge of Verilog HDL . Proc. of 10th Annual IEEE LICS(1995) , 136\u2013145. Michael J.\u00a0C. Gordon. 1995. The semantic challenge of Verilog HDL. Proc. of 10th Annual IEEE LICS(1995), 136\u2013145."},{"key":"e_1_3_2_1_28_1","article-title":"Relating Event and Trace Semantics of Hardware Description","volume":"45","author":"Gordon Michael","year":"2002","unstructured":"Michael J.\u00a0C. Gordon . 2002 . Relating Event and Trace Semantics of Hardware Description Languages. Comput. J. 45 , 1 (01 2002), 27\u201336. Michael J.\u00a0C. Gordon. 2002. Relating Event and Trace Semantics of Hardware Description Languages. Comput. J. 45, 1 (01 2002), 27\u201336.","journal-title":"Languages. Comput. J."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Ian Graves Adam\u00a0M. Procter William Harrison and Gerard Allwein. 2015. Provably Correct Development of Reconfigurable Hardware Designs via Equational Reasoning. In FPT. 160\u2013171.  Ian Graves Adam\u00a0M. Procter William Harrison and Gerard Allwein. 2015. Provably Correct Development of Reconfigurable Hardware Designs via Equational Reasoning. In FPT. 160\u2013171.","DOI":"10.1109\/FPT.2015.7393143"},{"key":"e_1_3_2_1_30_1","volume-title":"IEEE Symposium on FPGAs for Custom Computing Machines (FCCM). IEEE Computer Society.","author":"Greaves David","year":"2008","unstructured":"David Greaves and Satnam Singh . 2008 . Kiwi: Synthesis of FPGA Circuits from Parallel Programs . In IEEE Symposium on FPGAs for Custom Computing Machines (FCCM). IEEE Computer Society. David Greaves and Satnam Singh. 2008. Kiwi: Synthesis of FPGA Circuits from Parallel Programs. In IEEE Symposium on FPGAs for Custom Computing Machines (FCCM). IEEE Computer Society."},{"key":"e_1_3_2_1_31_1","first-page":"2","article-title":"A reflective functional language for hardware design and theorem proving","volume":"16","author":"Grundy Jim","year":"2006","unstructured":"Jim Grundy , Tom Melham , and John O\u2019leary . 2006 . A reflective functional language for hardware design and theorem proving . J. Funct. Program. 16 , 2 (March 2006), 157\u2013196. Jim Grundy, Tom Melham, and John O\u2019leary. 2006. A reflective functional language for hardware design and theorem proving. J. Funct. Program. 16, 2 (March 2006), 157\u2013196.","journal-title":"J. Funct. Program."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"W. Harrison. 2006. The Essence of Multitasking. In Algebraic Methodology and Software Technology. 158\u2013172.  W. Harrison. 2006. The Essence of Multitasking. In Algebraic Methodology and Software Technology. 158\u2013172.","DOI":"10.1007\/11784180_14"},{"key":"e_1_3_2_1_34_1","unstructured":"William Harrison. 2021. Device Calculus Codebase. Available from https:\/\/www.dropbox.com\/s\/j121q0p87z9k90b\/codebase.tar.gz?dl=1.  William Harrison. 2021. Device Calculus Codebase. Available from https:\/\/www.dropbox.com\/s\/j121q0p87z9k90b\/codebase.tar.gz?dl=1."},{"volume-title":"Proceedings of the Design, Automation, and Test Europe (DATE) Conference.","author":"L.","key":"e_1_3_2_1_35_1","unstructured":"William\u00a0 L. Harrison and Gerard Allwein. 2020. Verifiable Security Templates for Hardware . In Proceedings of the Design, Automation, and Test Europe (DATE) Conference. William\u00a0L. Harrison and Gerard Allwein. 2020. Verifiable Security Templates for Hardware. In Proceedings of the Design, Automation, and Test Europe (DATE) Conference."},{"key":"e_1_3_2_1_36_1","volume-title":"Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE).","author":"Herklotz Yann","year":"2021","unstructured":"Yann Herklotz and John Wickerson . 2021 . High-level synthesis tools should be proven correct . In Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE). Yann Herklotz and John Wickerson. 2021. High-level synthesis tools should be proven correct. In Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE)."},{"key":"e_1_3_2_1_37_1","unstructured":"[\n  37\n  ]  Bluespec Homepage.2017. http:\/\/bluespec.com.  [37] Bluespec Homepage.2017. http:\/\/bluespec.com."},{"volume-title":"2017 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). 209\u2013216","author":"Izraelevitz A.","key":"e_1_3_2_1_38_1","unstructured":"A. Izraelevitz , J. Koenig , P. Li , R. Lin , A. Wang , A. Magyar , D. Kim , C. Schmidt , C. Markley , J. Lawson , and J. Bachrach . 2017. Reusability is FIRRTL ground: Hardware construction languages, compiler frameworks, and transformations . In 2017 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). 209\u2013216 . A. Izraelevitz, J. Koenig, P. Li, R. Lin, A. Wang, A. Magyar, D. Kim, C. Schmidt, C. Markley, J. Lawson, and J. Bachrach. 2017. Reusability is FIRRTL ground: Hardware construction languages, compiler frameworks, and transformations. In 2017 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). 209\u2013216."},{"key":"e_1_3_2_1_39_1","volume-title":"Contemporary Logic Design","author":"Katz H.","unstructured":"Randy\u00a0 H. Katz . 2000. Contemporary Logic Design ( 2 nd ed.). Addison-Wesley Longman Publishing Co., Inc. , Boston, MA, USA . Randy\u00a0H. Katz. 2000. Contemporary Logic Design(2nd ed.). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.","edition":"2"},{"key":"e_1_3_2_1_40_1","unstructured":"Wilayat Khan Alwen Tiu and David Sanan. [n.d.]. VeriFormal: An Executable Formal Model of a Hardware Description Language.  Wilayat Khan Alwen Tiu and David Sanan. [n.d.]. VeriFormal: An Executable Formal Model of a Hardware Description Language."},{"volume-title":"Formal Semantics for VHDL","author":"Kloos C.","key":"e_1_3_2_1_41_1","unstructured":"C. Kloos and P. Breuer( Eds .). 1995. Formal Semantics for VHDL . Kluwer Academic Publishers . C. Kloos and P. Breuer(Eds.). 1995. Formal Semantics for VHDL. Kluwer Academic Publishers."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97301"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_45_1","volume-title":"2019 IEEE\/ACM 7th International Conference on Formal Methods in Software Engineering (FormaliSE). 99\u2013108","author":"L\u00f6\u00f6w Andreas","year":"2019","unstructured":"Andreas L\u00f6\u00f6w and Magnus\u00a0 O. Myreen . 2019 . A Proof-Producing Translator for Verilog Development in HOL . In 2019 IEEE\/ACM 7th International Conference on Formal Methods in Software Engineering (FormaliSE). 99\u2013108 . Andreas L\u00f6\u00f6w and Magnus\u00a0O. Myreen. 2019. A Proof-Producing Translator for Verilog Development in HOL. In 2019 IEEE\/ACM 7th International Conference on Formal Methods in Software Engineering (FormaliSE). 99\u2013108."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1955.tb03788.x"},{"key":"e_1_3_2_1_47_1","volume-title":"Proceedings of the 23rd International Conference on Implementation and Application of Functional Languages","author":"Megacz A.","year":"2012","unstructured":"A. Megacz . 2012 . Hardware Design with Generalized Arrows . In Proceedings of the 23rd International Conference on Implementation and Application of Functional Languages ( Lawrence, KS) (IFL\u201911). Springer-Verlag, Berlin, Heidelberg, 164\u2013180. https:\/\/doi.org\/10.1007\/978-3-642-34407-7_11 10.1007\/978-3-642-34407-7_11 A. Megacz. 2012. Hardware Design with Generalized Arrows. In Proceedings of the 23rd International Conference on Implementation and Application of Functional Languages (Lawrence, KS) (IFL\u201911). Springer-Verlag, Berlin, Heidelberg, 164\u2013180. https:\/\/doi.org\/10.1007\/978-3-642-34407-7_11"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512941"},{"volume-title":"Principles of Program Analysis","author":"Nielson Flemming","key":"e_1_3_2_1_49_1","unstructured":"Flemming Nielson , Hanne\u00a0 R. Nielson , and Chris Hankin . 2010. Principles of Program Analysis . Springer . Flemming Nielson, Hanne\u00a0R. Nielson, and Chris Hankin. 2010. Principles of Program Analysis. Springer."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00055"},{"key":"e_1_3_2_1_51_1","first-page":"10","article-title":"Abstraction in Hardware System","volume":"54","author":"Nikhil S.","year":"2011","unstructured":"Rishiyur\u00a0 S. Nikhil . 2011 . Abstraction in Hardware System Design. Commun. ACM 54 , 10 (Oct. 2011), 36\u201344. https:\/\/doi.org\/10.1145\/2001269.2001284 10.1145\/2001269.2001284 Rishiyur\u00a0S. Nikhil. 2011. Abstraction in Hardware System Design. Commun. ACM 54, 10 (Oct. 2011), 36\u201344. https:\/\/doi.org\/10.1145\/2001269.2001284","journal-title":"Design. Commun. ACM"},{"key":"e_1_3_2_1_53_1","volume-title":"Article 33 (Jan.","author":"Procter Adam","year":"2017","unstructured":"Adam Procter , William Harrison , Ian Graves , Michela Becchi , and Gerard Allwein . 2017. A Principled Approach to Secure Multi-core Processor Design with ReWire. ACM TECS 16, 2 , Article 33 (Jan. 2017 ), 33:1\u201333:25\u00a0pages. Adam Procter, William Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. 2017. A Principled Approach to Secure Multi-core Processor Design with ReWire. ACM TECS 16, 2, Article 33 (Jan. 2017), 33:1\u201333:25\u00a0pages."},{"key":"e_1_3_2_1_54_1","volume-title":"High-Level Synthesis of FPGA Circuits with Multiple Clock Domains. In 2018 IEEE 26th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). 109\u2013116","author":"Ragheb O.","year":"2018","unstructured":"O. Ragheb and J.\u00a0 H. Anderson . 2018 . High-Level Synthesis of FPGA Circuits with Multiple Clock Domains. In 2018 IEEE 26th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). 109\u2013116 . O. Ragheb and J.\u00a0H. Anderson. 2018. High-Level Synthesis of FPGA Circuits with Multiple Clock Domains. In 2018 IEEE 26th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). 109\u2013116."},{"key":"e_1_3_2_1_55_1","volume-title":"ACM Workshop on Type Driven Development (TyDe).","author":"Reynolds Thomas","year":"2020","unstructured":"Thomas Reynolds , Rohit Chadha , William\u00a0 L. Harrison , and Gerard Allwein . 2020 . Strongly Bounded Termination with Applications to Security and Hardware Synthesis . In ACM Workshop on Type Driven Development (TyDe). Thomas Reynolds, Rohit Chadha, William\u00a0L. Harrison, and Gerard Allwein. 2020. Strongly Bounded Termination with Applications to Security and Hardware Synthesis. In ACM Workshop on Type Driven Development (TyDe)."},{"key":"e_1_3_2_1_56_1","volume-title":"Article 6 (Jan.","author":"Reynolds N.","year":"2019","unstructured":"Thomas\u00a0 N. Reynolds , Adam Procter , William Harrison , and Gerard Allwein . 2019. The Mechanized Marriage of Effects and Monads with Applications to High-assurance Hardware. ACM TECS 18, 1 , Article 6 (Jan. 2019 ), 26\u00a0pages. Thomas\u00a0N. Reynolds, Adam Procter, William Harrison, and Gerard Allwein. 2019. The Mechanized Marriage of Effects and Monads with Applications to High-assurance Hardware. ACM TECS 18, 1, Article 6 (Jan. 2019), 26\u00a0pages."},{"key":"e_1_3_2_1_57_1","first-page":"1","article-title":"Static consistency checking for Verilog wire interconnects\u2014Using dependent types to check the sanity of Verilog descriptions","volume":"24","author":"Salama Cherif","year":"2011","unstructured":"Cherif Salama , Gregory Malecha , Walid Taha , Jim Grundy , and John O\u2019Leary . 2011 . Static consistency checking for Verilog wire interconnects\u2014Using dependent types to check the sanity of Verilog descriptions . Higher-Order and Symbolic Computation 24 , 1 - 2 (2011), 81\u2013114. Cherif Salama, Gregory Malecha, Walid Taha, Jim Grundy, and John O\u2019Leary. 2011. Static consistency checking for Verilog wire interconnects\u2014Using dependent types to check the sanity of Verilog descriptions. Higher-Order and Symbolic Computation 24, 1-2 (2011), 81\u2013114.","journal-title":"Higher-Order and Symbolic Computation"},{"key":"e_1_3_2_1_58_1","volume-title":"US Department of Defense Trusted Microelectronics. In the Proceedings of the 17th Annual NDIA Systems Engineering Conference.","author":"Shanahan Raymond","year":"2014","unstructured":"Raymond Shanahan . 2014 . US Department of Defense Trusted Microelectronics. In the Proceedings of the 17th Annual NDIA Systems Engineering Conference. Raymond Shanahan. 2014. US Department of Defense Trusted Microelectronics. In the Proceedings of the 17th Annual NDIA Systems Engineering Conference."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"crossref","unstructured":"Mary Sheeran. 1984. muFP A Language for VLSI Design. In LISP and Functional Programming. 104\u2013112.  Mary Sheeran. 1984. muFP A Language for VLSI Design. In LISP and Functional Programming. 104\u2013112.","DOI":"10.1145\/800055.802026"},{"key":"e_1_3_2_1_60_1","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"Stoy E.","year":"1977","unstructured":"Joseph\u00a0 E. Stoy . 1977 . Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory . MIT Press . Joseph\u00a0E. Stoy. 1977. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press."},{"key":"e_1_3_2_1_61_1","volume-title":"Design Automation and Test in Europe (DATE","author":"Ungureanu George","year":"2017","unstructured":"George Ungureanu and Ingo Sander . 2017. A Layered Formal Framework for Modeling of Cyber-Physical Systems . In Design Automation and Test in Europe (DATE 2017 ). Lausanne , Switzerland . George Ungureanu and Ingo Sander. 2017. A Layered Formal Framework for Modeling of Cyber-Physical Systems. In Design Automation and Test in Europe (DATE 2017). Lausanne, Switzerland."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_2"},{"key":"e_1_3_2_1_63_1","volume-title":"Understanding Clock Domain Crossing Issues. The EE Times (24","author":"Verma Saurabh","year":"2007","unstructured":"Saurabh Verma and Ashima Dabare . 2007. Understanding Clock Domain Crossing Issues. The EE Times (24 Dec. 2007 ). https:\/\/www.eetimes.com\/understanding-clock-domain-crossing-issues\/ Saurabh Verma and Ashima Dabare. 2007. Understanding Clock Domain Crossing Issues. The EE Times (24 Dec. 2007). https:\/\/www.eetimes.com\/understanding-clock-domain-crossing-issues\/"},{"key":"e_1_3_2_1_64_1","volume-title":"Field-Programmable Custom Computing Machines (FCCM), 2010 18th IEEE Annual International Symposium on. 127\u2013134","author":"Villarreal J.","year":"2010","unstructured":"J. Villarreal , A. Park , W. Najjar , and R. Halstead . 2010. Designing Modular Hardware Accelerators in C with ROCCC 2.0 . In Field-Programmable Custom Computing Machines (FCCM), 2010 18th IEEE Annual International Symposium on. 127\u2013134 . https:\/\/doi.org\/10.1109\/FCCM. 2010 .28 10.1109\/FCCM.2010.28 J. Villarreal, A. Park, W. Najjar, and R. Halstead. 2010. Designing Modular Hardware Accelerators in C with ROCCC 2.0. In Field-Programmable Custom Computing Machines (FCCM), 2010 18th IEEE Annual International Symposium on. 127\u2013134. https:\/\/doi.org\/10.1109\/FCCM.2010.28"},{"key":"e_1_3_2_1_65_1","unstructured":"Phillip Wadler Wen Kokke and Jeremy Siek. 2021. Programming Language Foundations in Agda. https:\/\/plfa.github.io.  Phillip Wadler Wen Kokke and Jeremy Siek. 2021. Programming Language Foundations in Agda. https:\/\/plfa.github.io."},{"key":"e_1_3_2_1_66_1","volume-title":"FPM: A Flexible Programming Model for MPSoC on FPGA. In Parallel and Distributed Processing Symposium Workshops PhD Forum (IPDPSW)","author":"Wang C.","year":"2012","unstructured":"C. Wang , X. Li , J. Zhang , P. Chen , X. Feng , and X. Zhou . 2012 . FPM: A Flexible Programming Model for MPSoC on FPGA. In Parallel and Distributed Processing Symposium Workshops PhD Forum (IPDPSW) , 2012 IEEE 26th International. 477\u2013484. C. Wang, X. Li, J. Zhang, P. Chen, X. Feng, and X. Zhou. 2012. FPM: A Flexible Programming Model for MPSoC on FPGA. In Parallel and Distributed Processing Symposium Workshops PhD Forum (IPDPSW), 2012 IEEE 26th International. 477\u2013484."},{"volume-title":"The formal semantics of programming languages: an introduction","author":"Winskel Glynn","key":"e_1_3_2_1_67_1","unstructured":"Glynn Winskel . 1993. The formal semantics of programming languages: an introduction . MIT Press . Glynn Winskel. 1993. The formal semantics of programming languages: an introduction.MIT Press."},{"key":"e_1_3_2_1_68_1","unstructured":"Xilinx Corporation 2021. Vivado High-Level Synthesis. http:\/\/www.xilinx.com\/products\/design-tools\/vivado\/integration\/esl-design.html.  Xilinx Corporation 2021. Vivado High-Level Synthesis. http:\/\/www.xilinx.com\/products\/design-tools\/vivado\/integration\/esl-design.html."},{"volume-title":"11th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS\u201906)","author":"Zhu Huibiao","key":"e_1_3_2_1_69_1","unstructured":"Huibiao Zhu , Jifeng He , and J. Bowen . 2006. From algebraic semantics to denotational semantics for Verilog . In 11th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS\u201906) . 341\u2013360. Huibiao Zhu, Jifeng He, and J. Bowen. 2006. From algebraic semantics to denotational semantics for Verilog. In 11th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS\u201906). 341\u2013360."}],"event":{"name":"PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming","acronym":"PPDP 2021","location":"Tallinn Estonia"},"container-title":["23rd International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479417","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3479394.3479417","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479417"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,6]]},"references-count":65,"alternative-id":["10.1145\/3479394.3479417","10.1145\/3479394"],"URL":"https:\/\/doi.org\/10.1145\/3479394.3479417","relation":{},"subject":[],"published":{"date-parts":[[2021,9,6]]},"assertion":[{"value":"2021-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}