{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:05Z","timestamp":1750221305668,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T00:00:00Z","timestamp":1515369600000},"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":[[2018,1,8]]},"DOI":"10.1145\/3167093","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"280-292","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A two-level logic perspective on (simultaneous) substitutions"],"prefix":"10.1145","author":[{"given":"Kaustuv","family":"Chaudhuri","sequence":"first","affiliation":[{"name":"Inria, France \/ \u00c9cole Polytechnique, France"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_2_2_1","article-title":"Abella: A System for Reasoning about Relational Specifications","volume":"7","author":"Baelde David","year":"2014","unstructured":"David Baelde , Kaustuv Chaudhuri , Andrew Gacek , Dale Miller , Gopalan Nadathur , Alwen Tiu , and Yuting Wang . 2014 . Abella: A System for Reasoning about Relational Specifications . Journal of Formalized Reasoning 7 , 2 (2014). David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. 2014. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning 7, 2 (2014).","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_3_2_2_3_1","unstructured":"Horace Blanc and Beniamino Accattoli. 2016. Relating \u03c0 -calculus and \u03bb-calculus by means of the linear substitution calculus. Available at https:\/\/github.com\/abella-prover\/abella\/tree\/master\/examples\/ process-calculi\/pic_lambda . (2016).  Horace Blanc and Beniamino Accattoli. 2016. Relating \u03c0 -calculus and \u03bb-calculus by means of the linear substitution calculus. Available at https:\/\/github.com\/abella-prover\/abella\/tree\/master\/examples\/ process-calculi\/pic_lambda . (2016)."},{"key":"e_1_3_2_2_4_1","article-title":"The Locally Nameless Representation","author":"Chargu\u00e9raud Arthur","year":"2011","unstructured":"Arthur Chargu\u00e9raud . 2011 . The Locally Nameless Representation . Journal of Automated Reasoning ( May 2011), 1\u201346. Arthur Chargu\u00e9raud. 2011. The Locally Nameless Representation. Journal of Automated Reasoning (May 2011), 1\u201346.","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_2_2_5_1","volume-title":"Formalized Meta-Theory of Sequent Calculi for Substructural Logics. In Workshop on Logical and Semantic Frameworks, with Applications (LSFA) . Post proceedings version","author":"Chaudhuri Kaustuv","year":"2016","unstructured":"Kaustuv Chaudhuri , Leonardo Lima , and Giselle Reis . 2016 . Formalized Meta-Theory of Sequent Calculi for Substructural Logics. In Workshop on Logical and Semantic Frameworks, with Applications (LSFA) . Post proceedings version to appear; Formalization https: \/\/github.com\/meta-logic\/abella-reasoning . Kaustuv Chaudhuri, Leonardo Lima, and Giselle Reis. 2016. Formalized Meta-Theory of Sequent Calculi for Substructural Logics. In Workshop on Logical and Semantic Frameworks, with Applications (LSFA) . Post proceedings version to appear; Formalization https: \/\/github.com\/meta-logic\/abella-reasoning ."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_24"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9218-1"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_17"},{"volume-title":"Proc. ICALP\u201901 (Lecture Notes in Computer Science)","author":"Honsell Furio","key":"e_1_3_2_2_17_1","unstructured":"Furio Honsell , Marino Miculan , and Ivan Scagnetto . 2001. An axiomatic approach to metareasoning on systems in higher-order abstract syntax . In Proc. ICALP\u201901 (Lecture Notes in Computer Science) . Springer , 963\u2013 978. Furio Honsell, Marino Miculan, and Ivan Scagnetto. 2001. An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In Proc. ICALP\u201901 (Lecture Notes in Computer Science). Springer, 963\u2013 978."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/111360.111369"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1947873.1947878"},{"volume-title":"Programming with HigherOrder Logic","author":"Miller Dale","key":"e_1_3_2_2_20_1","unstructured":"Dale Miller and Gopalan Nadathur . 2012. Programming with HigherOrder Logic . Cambridge University Press . Dale Miller and Gopalan Nadathur. 2012. Programming with HigherOrder Logic . Cambridge University Press."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364406.2364411"},{"key":"e_1_3_2_2_22_1","unstructured":"Alberto Momigliano Brigitte Pientka and David Thibodeau. 2017. A case-study in programming coinductive proofs: Howe\u2019s method. Submitted. (2017).  Alberto Momigliano Brigitte Pientka and David Thibodeau. 2017. A case-study in programming coinductive proofs: Howe\u2019s method. Submitted. (2017)."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"volume-title":"Handbook of Automated Reasoning (in 2 volumes)","author":"Pfenning Frank","key":"e_1_3_2_2_24_1","unstructured":"Frank Pfenning . 2001. Logical Frameworks . In Handbook of Automated Reasoning (in 2 volumes) , John Alan Robinson and Andrei Voronkov (Eds.). Elsevier and MIT Press , 1063\u20131147. Frank Pfenning. 2001. Logical Frameworks. In Handbook of Automated Reasoning (in 2 volumes), John Alan Robinson and Andrei Voronkov (Eds.). Elsevier and MIT Press, 1063\u20131147."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pitts Andrew M.","key":"e_1_3_2_2_29_1","unstructured":"Andrew M. Pitts . 2011. Howe\u2019s method for higher-order languages . In Advanced Topics in Bisimulation and Coinduction , David Sangiorgi and Jan Rutten (Eds.). Cambridge University Press , Chapter 5, 197\u2013232. Andrew M. Pitts. 2011. Howe\u2019s method for higher-order languages. In Advanced Topics in Bisimulation and Coinduction, David Sangiorgi and Jan Rutten (Eds.). Cambridge University Press, Chapter 5, 197\u2013232."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2631172.2631181"},{"key":"e_1_3_2_2_32_1","volume-title":"Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Proceedings of ITP\u201915 (Lecture Notes in Artificial Intelligence)","author":"Sch\u00e4fer Steven","year":"2015","unstructured":"Steven Sch\u00e4fer , Tobias Tebbi , and Gert Smolka . 2015 . Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Proceedings of ITP\u201915 (Lecture Notes in Artificial Intelligence) , Xingyuan Zhang and Christian Urban (Eds.). Springer . Steven Sch\u00e4fer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Proceedings of ITP\u201915 (Lecture Notes in Artificial Intelligence), Xingyuan Zhang and Christian Urban (Eds.). Springer."},{"key":"e_1_3_2_2_33_1","volume-title":"Rules of Definitional Reflection. In 8th Symp. on Logic in Computer Science, M. Vardi (Ed.). IEEE Computer Society Press, IEEE, 222\u2013232","author":"Schroeder-Heister Peter","year":"1993","unstructured":"Peter Schroeder-Heister . 1993 . Rules of Definitional Reflection. In 8th Symp. on Logic in Computer Science, M. Vardi (Ed.). IEEE Computer Society Press, IEEE, 222\u2013232 . Peter Schroeder-Heister. 1993. Rules of Definitional Reflection. In 8th Symp. on Logic in Computer Science, M. Vardi (Ed.). IEEE Computer Society Press, IEEE, 222\u2013232."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_4"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505889"}],"event":{"name":"CPP '18: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Los Angeles CA USA","acronym":"CPP '18"},"container-title":["Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167093","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167093","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:28Z","timestamp":1750212808000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167093"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":34,"alternative-id":["10.1145\/3167093","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167093","relation":{},"subject":[],"published":{"date-parts":[[2018,1,8]]},"assertion":[{"value":"2018-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}