{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:31Z","timestamp":1750221271146,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,9,29]],"date-time":"2017-09-29T00:00:00Z","timestamp":1506643200000},"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":[[2017,9,29]]},"DOI":"10.1145\/3127041.3127048","type":"proceedings-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T12:34:00Z","timestamp":1506515640000},"page":"122-131","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A core calculus for secure hardware"],"prefix":"10.1145","author":[{"given":"Thomas N.","family":"Reynolds","sequence":"first","affiliation":[{"name":"University of Missouri"}]},{"given":"Adam","family":"Procter","sequence":"additional","affiliation":[{"name":"University of Missouri"}]},{"given":"William L.","family":"Harrison","sequence":"additional","affiliation":[{"name":"University of Missouri"}]},{"given":"Gerard","family":"Allwein","sequence":"additional","affiliation":[{"name":"US Naval Research Laboratory"}]}],"member":"320","published-online":{"date-parts":[[2017,9,29]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535839"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Thomas Braibant and Adam Chlipala. 2013. Formal Verification of Hardware Synthesis. In CAV. 213--228.  Thomas Braibant and Adam Chlipala. 2013. Formal Verification of Hardware Synthesis. In CAV . 213--228.","DOI":"10.1007\/978-3-642-39799-8_14"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_4"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005441"},{"key":"e_1_3_2_1_6_1","volume-title":"http:\/\/bluespec.com. (July","author":"DL.","year":"2017","unstructured":"Bluespec functional H DL. 2017. http:\/\/bluespec.com. (July 2017 ). Bluespec functional HDL. 2017. http:\/\/bluespec.com. (July 2017)."},{"key":"e_1_3_2_1_7_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":"Unwinding and Inference Control. In IEEE Symp. on Security and Privacy. 75--86","author":"Goguen J.A.","key":"e_1_3_2_1_8_1","unstructured":"J.A. Goguen and J. Meseguer . 1984 . Unwinding and Inference Control. In IEEE Symp. on Security and Privacy. 75--86 . J.A. Goguen and J. Meseguer. 1984. Unwinding and Inference Control. In IEEE Symp. on Security and Privacy. 75--86."},{"volume-title":"Proc. of the 18th International Conf. on Fundamentals of Computation Theory. 276--287","author":"Goncharov S.","key":"e_1_3_2_1_9_1","unstructured":"S. Goncharov and L. Schr\u00f6der . 2011. A coinductive calculus for asynchronous side-effecting processes . In Proc. of the 18th International Conf. on Fundamentals of Computation Theory. 276--287 . S. Goncharov and L. Schr\u00f6der. 2011. A coinductive calculus for asynchronous side-effecting processes. In Proc. of the 18th International Conf. on Fundamentals of Computation Theory. 276--287."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/788017.788782"},{"volume-title":"IEEE Inter. Conf. on Field-Programmable Technology (ICFPT). 160--171","author":"Graves I.","key":"e_1_3_2_1_11_1","unstructured":"I. Graves , W. Harrison , A. Procter , and G. Allwein . 2015. Provably Correct Development of Reconfigurable Hardware Designs via Equational Reasoning . In IEEE Inter. Conf. on Field-Programmable Technology (ICFPT). 160--171 . I. Graves, W. Harrison, A. Procter, and G. Allwein. 2015. Provably Correct Development of Reconfigurable Hardware Designs via Equational Reasoning. In IEEE Inter. Conf. on Field-Programmable Technology (ICFPT). 160--171."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16214-0_4"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11784180_14"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"W. Harrison and J. Hook. 2009. Achieving information flow security through monadic control of effects. JCS 17 (Oct 2009) 599--653. Issue 5.   W. Harrison and J. Hook. 2009. Achieving information flow security through monadic control of effects. JCS 17 (Oct 2009) 599--653. Issue 5.","DOI":"10.3233\/JCS-2009-0356"},{"volume-title":"11th Inter. Symp. on Reconfigurable Communication-centric Systems-on-Chip.","author":"Harrison W.","key":"e_1_3_2_1_15_1","unstructured":"W. Harrison , A. Procter , I. Graves , M. Becchi , and G. Allwein . 2016. A Programming Model for Reconfigurable Computing Based in Functional Concurrency . In 11th Inter. Symp. on Reconfigurable Communication-centric Systems-on-Chip. W. Harrison, A. Procter, I. Graves, M. Becchi, and G. Allwein. 2016. A Programming Model for Reconfigurable Computing Based in Functional Concurrency. In 11th Inter. Symp. on Reconfigurable Communication-centric Systems-on-Chip."},{"key":"e_1_3_2_1_17_1","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.","DOI":"10.1007\/978-1-4615-2237-9"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2011.68"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541947"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993512"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/174889"},{"volume-title":"Foundations for Programming Languages","author":"Mitchell J.","key":"e_1_3_2_1_24_1","unstructured":"J. Mitchell . 1996. Foundations for Programming Languages . MIT Press Cambridge . J. Mitchell. 1996. Foundations for Programming Languages. MIT Press Cambridge."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_26_1","volume-title":"personal communication. (March","author":"Myers A.","year":"2017","unstructured":"A. Myers . 2017. personal communication. (March 2017 ). A. Myers. 2017. personal communication. (March 2017)."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_28_1","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.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"e_1_3_2_1_29_1","unstructured":"Simon Peyton Jones (Ed.). 2003. Haskell 98 Language and Libraries the Revised Report. Cambridge University Press. 272 pages.  Simon Peyton Jones (Ed.). 2003. Haskell 98 Language and Libraries the Revised Report. Cambridge University Press. 272 pages."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967497"},{"key":"e_1_3_2_1_32_1","volume-title":"https:\/\/goo.gl\/FYf6xU. (July","author":"DE.","year":"2017","unstructured":"Code repository for MEMOCO DE. 2017. https:\/\/goo.gl\/FYf6xU. (July 2017 ). https:\/\/goo.gl\/FYf6xU Code repository for MEMOCODE. 2017. https:\/\/goo.gl\/FYf6xU. (July 2017). https:\/\/goo.gl\/FYf6xU"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516507.1516510"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.11.020"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_30"},{"key":"e_1_3_2_1_37_1","unstructured":"VST {n. d.}. Verified Software Toolchain. http:\/\/vst.cs.princeton.edu. ({n. d.}).  VST {n. d.}. Verified Software Toolchain. http:\/\/vst.cs.princeton.edu. ({n. d.})."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_15"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289429"},{"key":"e_1_3_2_1_40_1","volume-title":"Technical Report 2014-04-10. Dept. of Computer Science","author":"Zhang D.","year":"2014","unstructured":"D. Zhang , Y. Wang , G. E. Suh , and A. Myers . 2014 . A Hardware Design Language for Efficient Control of Timing Channels. Technical Report 2014-04-10. Dept. of Computer Science , Cornell University. Extended version of the authors' ASPLOS 15 paper. D. Zhang, Y. Wang, G. E. Suh, and A. Myers. 2014. A Hardware Design Language for Efficient Control of Timing Channels. Technical Report 2014-04-10. Dept. of Computer Science, Cornell University. Extended version of the authors' ASPLOS15 paper."}],"event":{"name":"MEMOCODE '17: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"],"location":"Vienna Austria","acronym":"MEMOCODE '17"},"container-title":["Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127041.3127048","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3127041.3127048","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:06Z","timestamp":1750212666000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127041.3127048"}},"subtitle":["its formal semantics and proof system"],"short-title":[],"issued":{"date-parts":[[2017,9,29]]},"references-count":38,"alternative-id":["10.1145\/3127041.3127048","10.1145\/3127041"],"URL":"https:\/\/doi.org\/10.1145\/3127041.3127048","relation":{},"subject":[],"published":{"date-parts":[[2017,9,29]]},"assertion":[{"value":"2017-09-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}