{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:15Z","timestamp":1750220595486,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,8,9]],"date-time":"2020-08-09T00:00:00Z","timestamp":1596931200000},"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":[[2020,8,23]]},"DOI":"10.1145\/3406089.3409029","type":"proceedings-article","created":{"date-parts":[[2020,7,31]],"date-time":"2020-07-31T04:07:40Z","timestamp":1596168460000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Strongly bounded termination with applications to security and hardware synthesis"],"prefix":"10.1145","author":[{"given":"Thomas","family":"Reynolds","sequence":"first","affiliation":[{"name":"University of Missouri, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William L.","family":"Harrison","sequence":"additional","affiliation":[{"name":"Oak Ridge National Laboratory, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rohit","family":"Chadha","sequence":"additional","affiliation":[{"name":"University of Missouri, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerard","family":"Allwein","sequence":"additional","affiliation":[{"name":"US Naval Research Laboratory, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,8,9]]},"reference":[{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Andreas Abel. 2008. Semi-continuous Sized Types and Termination. Logical Methods in Computer Science 4 2 ( 2008 ) 1-33.  Andreas Abel. 2008. Semi-continuous Sized Types and Termination. Logical Methods in Computer Science 4 2 ( 2008 ) 1-33.","DOI":"10.2168\/LMCS-4(2:3)2008"},{"volume-title":"27th ACM SIGPLAN-SIGACT POPL. 40-53.","author":"Agat Johan","key":"e_1_3_2_1_3_1","unstructured":"Johan Agat . 2000. Transforming Out Timing Leaks . In 27th ACM SIGPLAN-SIGACT POPL. 40-53. Johan Agat. 2000. Transforming Out Timing Leaks. In 27th ACM SIGPLAN-SIGACT POPL. 40-53."},{"volume-title":"The designer's guide to VHDL","author":"Ashenden Peter J","key":"e_1_3_2_1_4_1","unstructured":"Peter J Ashenden . 2010. The designer's guide to VHDL . Vol. 3 . Morgan Kaufmann . Peter J Ashenden. 2010. The designer's guide to VHDL. Vol. 3. Morgan Kaufmann."},{"key":"e_1_3_2_1_5_1","first-page":"17","article-title":"Using Rewriting to Synthesize Functional Languages to Digital Circuits","volume":"8322","author":"Baaij C.","year":"2014","unstructured":"C. Baaij and J. Kuper . 2014 . Using Rewriting to Synthesize Functional Languages to Digital Circuits . In Trends in Fun. Prog. (LNCS) , Vol. 8322. 17 - 33 . C. Baaij and J. Kuper. 2014. Using Rewriting to Synthesize Functional Languages to Digital Circuits. In Trends in Fun. Prog. (LNCS), Vol. 8322. 17-33.","journal-title":"Trends in Fun. Prog. (LNCS)"},{"volume-title":"Design Automation Conference (DAC). 1216-1225","author":"Bachrach J.","key":"e_1_3_2_1_6_1","unstructured":"J. Bachrach , H. Vo , B. Richards , Y. Lee , A. Waterman , R. Avizienis , J. Wawrzynek , and K. Asanovic . 2012. Chisel: constructing hardware in a Scala embedded language . In Design Automation Conference (DAC). 1216-1225 . J. Bachrach, H. Vo, B. Richards, Y. Lee, A. Waterman, R. Avizienis, J. Wawrzynek, and K. Asanovic. 2012. Chisel: constructing hardware in a Scala embedded language. In Design Automation Conference (DAC). 1216-1225."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_35"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Barthe G. Frade M. J. Gime\u02dcnez E. Pinto L. and Uustalu T. 2004. Type-based termination of recursive definitions. Math. Struct. in CS 14 1 ( 2004 ) 97-141.  Barthe G. Frade M. J. Gime\u02dcnez E. Pinto L. and Uustalu T. 2004. Type-based termination of recursive definitions. Math. Struct. in CS 14 1 ( 2004 ) 97-141.","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"volume-title":"44th ACM SIGPLAN POPL. 316-329.","author":"\u00c7i\u00e7ek Ezgi","key":"e_1_3_2_1_10_1","unstructured":"Ezgi \u00c7i\u00e7ek , Gilles Barthe , Marco Gaboardi , Deepak Garg , and Jan Hofmann . 2017. Relational Cost Analysis . In 44th ACM SIGPLAN POPL. 316-329. Ezgi \u00c7i\u00e7ek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hofmann. 2017. Relational Cost Analysis. In 44th ACM SIGPLAN POPL. 316-329."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58085-9_72"},{"volume-title":"Combinatory Logic. Studies in Logic and the Foundations of Mathematics","author":"Feys Haskell","key":"e_1_3_2_1_12_1","unstructured":"Curry, Haskell B. and Feys , R . 1958 . Combinatory Logic. Studies in Logic and the Foundations of Mathematics , Vol. I . North-Holland Publishing Company. Curry, Haskell B. and Feys, R. 1958. Combinatory Logic. Studies in Logic and the Foundations of Mathematics, Vol. I. North-Holland Publishing Company."},{"volume-title":"Combinatory Logic. Studies in Logic and the Foundations of Mathematics","author":"Haskell B., Hindley, J.","key":"e_1_3_2_1_13_1","unstructured":"Curry, Haskell B., Hindley, J. R., and Seldin, J. P . 1972 . Combinatory Logic. Studies in Logic and the Foundations of Mathematics , Vol. II . North-Holland Publishing Company. Curry, Haskell B., Hindley, J. R., and Seldin, J. P. 1972. Combinatory Logic. Studies in Logic and the Foundations of Mathematics, Vol. II. North-Holland Publishing Company."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09510-1_15"},{"volume-title":"10th ACM SIGPLAN ICFP. 168-179.","author":"Diatchki Iavor S.","key":"e_1_3_2_1_15_1","unstructured":"Iavor S. Diatchki , Mark P. Jones , and Rebekah Leslie . 2005. Highlevel Views on Low-level Representations . In 10th ACM SIGPLAN ICFP. 168-179. Iavor S. Diatchki, Mark P. Jones, and Rebekah Leslie. 2005. Highlevel Views on Low-level Representations. In 10th ACM SIGPLAN ICFP. 168-179."},{"key":"e_1_3_2_1_17_1","first-page":"1583","volume-title":"Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS '18)","author":"Ferraiuolo A.","unstructured":"A. Ferraiuolo , M. Zhao , A. C. Myers , and G. E. Suh . 2018. HyperFlow: A Processor Architecture for Nonmalleable, Timing-Safe Information Flow Security . In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS '18) . 1583 - 1600 . A. Ferraiuolo, M. Zhao, A. C. Myers, and G. E. Suh. 2018. HyperFlow: A Processor Architecture for Nonmalleable, Timing-Safe Information Flow Security. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS '18). 1583-1600."},{"key":"e_1_3_2_1_18_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"},{"key":"e_1_3_2_1_19_1","first-page":"331","volume-title":"Proceedings of the 23rd European Symposium on Programming Languages and Systems","volume":"8410","author":"Dan","unstructured":"Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring . In Proceedings of the 23rd European Symposium on Programming Languages and Systems , Vol. 8410 . 331 - 350 . Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Proceedings of the 23rd European Symposium on Programming Languages and Systems, Vol. 8410. 331-350."},{"volume-title":"Structural recursive definitions in type theory","author":"Gim\u00e9nez Eduardo","key":"e_1_3_2_1_20_1","unstructured":"Eduardo Gim\u00e9nez . 1998. Structural recursive definitions in type theory . In Automata, Languages and Programming, Kim G. Larsen, Sven Skyum, and Glynn Winskel (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 397-408. Eduardo Gim\u00e9nez. 1998. Structural recursive definitions in type theory. In Automata, Languages and Programming, Kim G. Larsen, Sven Skyum, and Glynn Winskel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 397-408."},{"key":"e_1_3_2_1_21_1","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."},{"volume-title":"IEEE Inter. Conf. on Field-Programmable Technology (ICFPT). 160-171","author":"Graves I.","key":"e_1_3_2_1_22_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_23_1","volume-title":"Proving the Correctness of Reactive Systems Using Sized Types. In 23rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. 410-423","author":"Hughes John","year":"1996","unstructured":"John Hughes , Lars Pareto , and Amr Sabry . 1996 . Proving the Correctness of Reactive Systems Using Sized Types. In 23rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. 410-423 . John Hughes, Lars Pareto, and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In 23rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. 410-423."},{"key":"e_1_3_2_1_24_1","unstructured":"R.H. Katz and G. Borriello. 2005. Contemporary Logic Design. Pearson Prentice Hall.  R.H. Katz and G. Borriello. 2005. Contemporary Logic Design. Pearson Prentice Hall."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017753.1017794"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1955.tb03788.x"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34407-7_11"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90069-X"},{"volume-title":"Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy (SP). 710-728","author":"Ngo V. C.","key":"e_1_3_2_1_29_1","unstructured":"V. C. Ngo , M. Dehesa-Azuara , M. Fredrikson , and J. Hofmann . 2017 . Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy (SP). 710-728 . V. C. Ngo, M. Dehesa-Azuara, M. Fredrikson, and J. Hofmann. 2017. Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy (SP). 710-728."},{"volume-title":"Principles of Program Analysis","author":"Nielson Flemming","key":"e_1_3_2_1_30_1","unstructured":"Flemming Nielson , Hanne R. Nielson , and Chris Hankin . 2010. Principles of Program Analysis . Springer . Flemming Nielson, Hanne R. Nielson, and Chris Hankin. 2010. Principles of Program Analysis. Springer."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"A. Procter W. Harrison I. Graves M. Becchi and G. Allwein. 2017. A Principled Approach to Secure Multi-core Processor Design with ReWire. ACM TECS 16 2 Article 33 ( Feb. 2017 ) 33 : 1-33 :25 pages.  A. Procter W. Harrison I. Graves M. Becchi and G. Allwein. 2017. A Principled Approach to Secure Multi-core Processor Design with ReWire. ACM TECS 16 2 Article 33 ( Feb. 2017 ) 33 : 1-33 :25 pages.","DOI":"10.1145\/2967497"},{"key":"e_1_3_2_1_33_1","volume-title":"Giford","author":"Reistad Brian","year":"1994","unstructured":"Brian Reistad and David K . Giford . 1994 . Static Dependent Costs for Estimating Execution Time. SIGPLAN Lisp Pointers VII , 3 ( July 1994 ), 65-78. Brian Reistad and David K. Giford. 1994. Static Dependent Costs for Estimating Execution Time. SIGPLAN Lisp Pointers VII, 3 ( July 1994 ), 65-78."},{"key":"e_1_3_2_1_34_1","unstructured":"Thomas Reynolds. 2020. Bounded Time Calculus Coq Codebase. Available from htps:\/\/www.dropbox.com\/s\/l3f2nhghxkooxjh\/tyde20-code.tar. gz?dl=0.  Thomas Reynolds. 2020. Bounded Time Calculus Coq Codebase. Available from htps:\/\/www.dropbox.com\/s\/l3f2nhghxkooxjh\/tyde20-code.tar. gz?dl=0."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274282"},{"key":"e_1_3_2_1_37_1","volume-title":"Linear Sized Types in the Calculus of Constructions. In 12th Inter. Symp. on Functional and Logic Programming (FLOPS). 169-185","author":"Sacchini Jorge Luis","year":"2014","unstructured":"Jorge Luis Sacchini . 2014 . Linear Sized Types in the Calculus of Constructions. In 12th Inter. Symp. on Functional and Logic Programming (FLOPS). 169-185 . Jorge Luis Sacchini. 2014. Linear Sized Types in the Calculus of Constructions. In 12th Inter. Symp. on Functional and Logic Programming (FLOPS). 169-185."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802026"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930141"},{"key":"e_1_3_2_1_40_1","first-page":"355","volume-title":"Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98)","author":"Smith G.","unstructured":"G. Smith and D. Volpano . 1998. Secure Information Flow in a Multi-threaded Imperative Language . In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98) . 355 - 364 . G. Smith and D. Volpano. 1998. Secure Information Flow in a Multi-threaded Imperative Language. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98). 355-364."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"},{"volume-title":"Proceedings of the 33rd ACM SIGPLAN PLDI. 99-110","author":"Zhang D.","key":"e_1_3_2_1_43_1","unstructured":"D. Zhang , A. Askarov , and A. C. Myers . 2012. Language-based Control and Mitigation of Timing Channels . In Proceedings of the 33rd ACM SIGPLAN PLDI. 99-110 . D. Zhang, A. Askarov, and A. C. Myers. 2012. Language-based Control and Mitigation of Timing Channels. In Proceedings of the 33rd ACM SIGPLAN PLDI. 99-110."}],"event":{"name":"ICFP '20: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual Event USA","acronym":"ICFP '20"},"container-title":["Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406089.3409029","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406089.3409029","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:52Z","timestamp":1750195912000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406089.3409029"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,9]]},"references-count":39,"alternative-id":["10.1145\/3406089.3409029","10.1145\/3406089"],"URL":"https:\/\/doi.org\/10.1145\/3406089.3409029","relation":{},"subject":[],"published":{"date-parts":[[2020,8,9]]},"assertion":[{"value":"2020-08-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}