{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:46Z","timestamp":1750221046915,"version":"3.41.0"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,1,8]],"date-time":"2019-01-08T00:00:00Z","timestamp":1546905600000},"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":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,1,31]]},"abstract":"<jats:p>Constructing high-assurance, secure hardware remains a challenge, because to do so relies on both a verifiable means of hardware description and implementation. However, production hardware description languages (HDL) lack the formal underpinnings required by formal methods in security. Still, there is no such thing as high-assurance systems without high-assurance hardware. We present a core calculus of secure hardware description with its formal semantics, security type system, and mechanization in Coq. This calculus is the core of the functional HDL, ReWire, shown in previous work to have useful applications in reconfigurable computing. This work supports a full-fledged, formal methodology for producing high-assurance hardware.<\/jats:p>","DOI":"10.1145\/3274282","type":"journal-article","created":{"date-parts":[[2019,1,8]],"date-time":"2019-01-08T15:53:12Z","timestamp":1546962792000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["The Mechanized Marriage of Effects and Monads with Applications to High-assurance Hardware"],"prefix":"10.1145","volume":"18","author":[{"given":"Thomas N.","family":"Reynolds","sequence":"first","affiliation":[{"name":"University of Missouri"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Procter","sequence":"additional","affiliation":[{"name":"University of Missouri"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William L.","family":"Harrison","sequence":"additional","affiliation":[{"name":"University of Missouri"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerard","family":"Allwein","sequence":"additional","affiliation":[{"name":"U.S. Naval Research Laboratory, , Washington DC, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,8]]},"reference":[{"unstructured":"D. Andrews. 2015. Will the future success of reconfigurable computing require a paradigm shift in our research community\u2019s thinking? Keynote address Applied Reconfigurable Computing. Retrieved from http:\/\/hthreads.csce.uark.edu\/mediawiki\/images\/d\/d8\/Arc-presentation.pdf.  D. Andrews. 2015. Will the future success of reconfigurable computing require a paradigm shift in our research community\u2019s thinking? Keynote address Applied Reconfigurable Computing. Retrieved from http:\/\/hthreads.csce.uark.edu\/mediawiki\/images\/d\/d8\/Arc-presentation.pdf.","key":"e_1_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1145\/2535838.2535839"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/978-3-642-45340-3_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1145\/2228360.2228584"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1145\/2436696.2443836"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1109\/ISCA.2008.34"},{"unstructured":"R. Bird and P. Wadler. 1988. Introduction to Functional Programming. Prentice Hall.   R. Bird and P. Wadler. 1988. Introduction to Functional Programming. Prentice Hall.","key":"e_1_2_1_7_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1145\/289423.289440"},{"volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV\u201913)","author":"Braibant T.","key":"e_1_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1007\/11757283_4"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/3110268"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/357766.351266"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/978-3-540-71067-7_16"},{"unstructured":"Coq {n.d.}. The Coq Proof Assistant. Retrieved from https:\/\/coq.inria.fr.  Coq {n.d.}. The Coq Proof Assistant. Retrieved from https:\/\/coq.inria.fr.","key":"e_1_2_1_14_1"},{"volume-title":"Infinite Objects in Type Theory","author":"Coquand T.","doi-asserted-by":"crossref","key":"e_1_2_1_15_1","DOI":"10.1007\/3-540-58085-9_72"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1017\/S0956796804005441"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/1577824.1577834"},{"volume-title":"Logic and Computer Science","author":"Gallier Jean H.","key":"e_1_2_1_18_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1145\/2543581.2543588"},{"volume-title":"Proceedings of the 24th International Conference on Field Programmable Logic and Applications (FPL\u201914)","author":"George N.","key":"e_1_2_1_20_1"},{"volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201916)","author":"Ghica D.","key":"e_1_2_1_21_1"},{"volume-title":"Codifying Guarded Definitions with Recursive Schemes","author":"Gim\u00e9nez E.","doi-asserted-by":"crossref","key":"e_1_2_1_22_1","DOI":"10.1007\/3-540-60579-7_3"},{"unstructured":"J.-Y. Girard Y. Lafont and P. Taylor. 1989. Proofs and Types. Vol. 7. Cambridge University Press Cambridge.   J.-Y. Girard Y. Lafont and P. Taylor. 1989. Proofs and Types. Vol. 7. Cambridge University Press Cambridge.","key":"e_1_2_1_23_1"},{"volume-title":"Proceedings of the IEEE Symposium on Security and Privacy. 75--86","author":"Goguen J. A.","key":"e_1_2_1_24_1"},{"volume-title":"Proceedings of the 18th International Conference on Fundamentals of Computation Theory. 276--287","author":"Goncharov S.","key":"e_1_2_1_25_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.5555\/788017.788782"},{"volume-title":"Proceedings of the IEEE International Conference on Field-Programmable Technology (ICFPT\u201915)","author":"Graves I.","key":"e_1_2_1_27_1"},{"volume":"9040","volume-title":"Proceedings of the Conference on Applied Reconfigurable Computing (LNCS)","author":"Graves I.","key":"e_1_2_1_28_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1007\/11784180_14"},{"key":"e_1_2_1_30_1","first-page":"5","article-title":"Achieving information flow security through monadic control of effects","volume":"17","author":"Harrison W.","year":"2009","journal-title":"J. Comput. Sci."},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.1145\/2990299.2990318"},{"volume-title":"Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip.","author":"Harrison W.","key":"e_1_2_1_32_1"},{"unstructured":"Bluespec Homepage. 2017. Retrieved from http:\/\/bluespec.com.  Bluespec Homepage. 2017. Retrieved from http:\/\/bluespec.com.","key":"e_1_2_1_33_1"},{"doi-asserted-by":"crossref","unstructured":"T. Huffmire C. Irvine T. Nguyen T. Levin R. Kastner and T. Sherwood. 2010. Handbook of FPGA Design Security. Springer.   T. Huffmire C. Irvine T. Nguyen T. Levin R. Kastner and T. Sherwood. 2010. Handbook of FPGA Design Security. Springer.","key":"e_1_2_1_35_1","DOI":"10.1007\/978-90-481-9157-4"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.1007\/11863908_28"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1016\/j.cose.2008.05.002"},{"doi-asserted-by":"crossref","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_2_1_38_1","DOI":"10.1007\/978-1-4615-2237-9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1109\/MM.2011.68"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1145\/1538788.1538814"},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1145\/2541940.2541947"},{"doi-asserted-by":"publisher","key":"e_1_2_1_42_1","DOI":"10.1145\/1993498.1993512"},{"doi-asserted-by":"publisher","key":"e_1_2_1_43_1","DOI":"10.1145\/199448.199528"},{"doi-asserted-by":"publisher","key":"e_1_2_1_44_1","DOI":"10.1007\/978-3-642-34407-7_11"},{"volume-title":"Higher Order Logic and Hardware Verification","author":"Melham T.","doi-asserted-by":"crossref","key":"e_1_2_1_45_1","DOI":"10.1017\/CBO9780511569845"},{"volume-title":"Foundations for Programming Languages","author":"Mitchell J.","key":"e_1_2_1_46_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_48_1","DOI":"10.1016\/0890-5401(91)90052-4"},{"unstructured":"A. Myers. 2017. personal communication.  A. Myers. 2017. personal communication.","key":"e_1_2_1_49_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_50_1","DOI":"10.1145\/1411204.1411237"},{"doi-asserted-by":"crossref","unstructured":"F. Nielson H. Nielson and C. Hankin. 1999. Principles of Program Analysis.   F. Nielson H. Nielson and C. Hankin. 1999. Principles of Program Analysis.","key":"e_1_2_1_51_1","DOI":"10.1007\/978-3-662-03811-6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_52_1","DOI":"10.1145\/1862876.1862877"},{"volume-title":"Proceedings of the Forum on Specification and Design Languages (FDL\u201913)","author":"Ouchani S.","key":"e_1_2_1_53_1"},{"unstructured":"S. Peyton Jones (Ed.). 2003. Haskell 98 Language and Libraries the Revised Report. Cambridge University Press.  S. Peyton Jones (Ed.). 2003. Haskell 98 Language and Libraries the Revised Report. Cambridge University Press.","key":"e_1_2_1_54_1"},{"unstructured":"B. C. Pierce C. Casinghino M. Gaboardi M. Greenberg C. Hri\u0163cu V. Sjoberg and B. Yorgey. 2015. Software Foundations. Electronic textbook.  B. C. Pierce C. Casinghino M. Gaboardi M. Greenberg C. Hri\u0163cu V. Sjoberg and B. Yorgey. 2015. Software Foundations. Electronic textbook.","key":"e_1_2_1_55_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_57_1","DOI":"10.1145\/2670529.2754970"},{"doi-asserted-by":"publisher","key":"e_1_2_1_58_1","DOI":"10.1145\/2967497"},{"unstructured":"Code repository for MEMOCODE. 2017. Retrieved from https:\/\/goo.gl\/FYf6xU.  Code repository for MEMOCODE. 2017. Retrieved from https:\/\/goo.gl\/FYf6xU.","key":"e_1_2_1_59_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_60_1","DOI":"10.1007\/s11334-011-0149-0"},{"doi-asserted-by":"publisher","key":"e_1_2_1_61_1","DOI":"10.1109\/JSAC.2002.806121"},{"doi-asserted-by":"publisher","key":"e_1_2_1_62_1","DOI":"10.1109\/TCAD.2003.819898"},{"doi-asserted-by":"publisher","key":"e_1_2_1_63_1","DOI":"10.1016\/j.entcs.2008.02.011"},{"doi-asserted-by":"publisher","key":"e_1_2_1_64_1","DOI":"10.1145\/1516507.1516510"},{"doi-asserted-by":"publisher","key":"e_1_2_1_65_1","DOI":"10.1016\/j.tcs.2008.11.020"},{"doi-asserted-by":"publisher","key":"e_1_2_1_66_1","DOI":"10.1145\/800055.802026"},{"doi-asserted-by":"publisher","key":"e_1_2_1_67_1","DOI":"10.1145\/1024393.1024404"},{"doi-asserted-by":"publisher","key":"e_1_2_1_68_1","DOI":"10.1007\/978-3-642-03359-9_30"},{"doi-asserted-by":"publisher","key":"e_1_2_1_69_1","DOI":"10.2307\/2271658"},{"volume-title":"Logic Colloquium (Lectures Notes in Mathematics)","author":"Tait W. W.","key":"e_1_2_1_70_1"},{"doi-asserted-by":"crossref","unstructured":"M. Tehranipoor and C. Wang. 2011. Introduction to Hardware Security and Trust. Springer Publishing Company Incorporated.   M. Tehranipoor and C. Wang. 2011. Introduction to Hardware Security and Trust. Springer Publishing Company Incorporated.","key":"e_1_2_1_71_1","DOI":"10.1007\/978-1-4419-8080-9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_72_1","DOI":"10.1145\/1669112.1669174"},{"doi-asserted-by":"publisher","key":"e_1_2_1_73_1","DOI":"10.1145\/2000064.2000087"},{"doi-asserted-by":"publisher","key":"e_1_2_1_74_1","DOI":"10.1145\/1508244.1508258"},{"doi-asserted-by":"publisher","key":"e_1_2_1_75_1","DOI":"10.1145\/1508244.1508258"},{"doi-asserted-by":"publisher","key":"e_1_2_1_76_1","DOI":"10.1109\/JPROC.2014.2331672"},{"doi-asserted-by":"publisher","key":"e_1_2_1_77_1","DOI":"10.5555\/353629.353648"},{"unstructured":"VST {n. d.}. Verified Software Toolchain. Retrieved from http:\/\/vst.cs.princeton.edu.  VST {n. d.}. Verified Software Toolchain. Retrieved from http:\/\/vst.cs.princeton.edu.","key":"e_1_2_1_78_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_79_1","DOI":"10.1007\/978-3-642-34281-3_15"},{"doi-asserted-by":"publisher","key":"e_1_2_1_80_1","DOI":"10.1145\/289423.289429"},{"volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","year":"1855","author":"Zeldovich N.","key":"e_1_2_1_81_1"},{"volume-title":"Proceedings of the 10th International Conference on Hardware\/Software Codesign and System Synthesis (CODES\u201915)","author":"Zhai K.","key":"e_1_2_1_82_1"},{"volume-title":"Technical Report 2014-04-10. Department of Computer Science","year":"2014","author":"Zhang D.","key":"e_1_2_1_83_1"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3274282","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3274282","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:44:06Z","timestamp":1750207446000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3274282"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,8]]},"references-count":80,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1,31]]}},"alternative-id":["10.1145\/3274282"],"URL":"https:\/\/doi.org\/10.1145\/3274282","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2019,1,8]]},"assertion":[{"value":"2017-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}