{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:12Z","timestamp":1750220652498,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,19]],"date-time":"2020-10-19T00:00:00Z","timestamp":1603065600000},"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,10,19]]},"DOI":"10.1145\/3427081.3427083","type":"proceedings-article","created":{"date-parts":[[2020,10,22]],"date-time":"2020-10-22T23:50:55Z","timestamp":1603410655000},"page":"9-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Syntax vs Semantics"],"prefix":"10.1145","author":[{"given":"Felipe","family":"Sasdelli","sequence":"first","affiliation":[{"name":"Universidade Federal de Ouro Preto"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maycon","family":"Amaro","sequence":"additional","affiliation":[{"name":"Universidade Federal de Ouro Preto"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elton","family":"Cardoso","sequence":"additional","affiliation":[{"name":"Programa de P\u00f3s-Gradua\u00e7\u00e3o em, Ci\u00eancia da Computa\u00e7\u00e3o, Universidade Federal de Ouro Preto"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samuel","family":"Feitosa","sequence":"additional","affiliation":[{"name":"Departamento de Inform\u00e1tica Ca\u00e7ador, Santa Catarina, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rodrigo","family":"Ribeiro","sequence":"additional","affiliation":[{"name":"Programa de P\u00f3s-Gradua\u00e7\u00e3o em, Ci\u00eancia da Computa\u00e7\u00e3o, Universidade Federal de Ouro Preto"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,22]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"23rd International Conference on Types for Proofs and Programs (TYPES 2017) (Leibniz International Proceedings in Informatics (LIPIcs))","author":"Allais Guillaume","year":"2017","unstructured":"Guillaume Allais . 2018. Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic . In 23rd International Conference on Types for Proofs and Programs (TYPES 2017) (Leibniz International Proceedings in Informatics (LIPIcs)) , Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi (Eds.), Vol. 104 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany , 1:1--1:22. https:\/\/doi.org\/10.4230\/LIPIcs.TYPES. 2017 .1 10.4230\/LIPIcs.TYPES.2017.1 Guillaume Allais. 2018. Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017) (Leibniz International Proceedings in Informatics (LIPIcs)), Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi (Eds.), Vol. 104. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 1:1--1:22. https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2017.1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009866"},{"key":"e_1_3_2_1_3_1","volume-title":"Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda. CoRR abs\/1601.07724","author":"Bernardy Jean-Philippe","year":"2016","unstructured":"Jean-Philippe Bernardy and Patrik Jansson . 2016. Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda. CoRR abs\/1601.07724 ( 2016 ). http:\/\/arxiv.org\/abs\/1601.07724 Jean-Philippe Bernardy and Patrik Jansson. 2016. Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda. CoRR abs\/1601.07724 (2016). http:\/\/arxiv.org\/abs\/1601.07724"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/2584504"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_6"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006285817788"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.09.002"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1947873.1947907"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000066"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01565428"},{"key":"e_1_3_2_1_15_1","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier Georges","year":"2010","unstructured":"Georges Gonthier and Assia Mahboubi . 2010 . An introduction to small scale reflection in Coq . J. Formalized Reasoning 3 , 2 (2010), 95 -- 152 . https:\/\/doi.org\/10.6092\/issn.1972-5787\/1979 10.6092\/issn.1972-5787 Georges Gonthier and Assia Mahboubi. 2010. An introduction to small scale reflection in Coq. J. Formalized Reasoning 3, 2 (2010), 95--152. https:\/\/doi.org\/10.6092\/issn.1972-5787\/1979","journal-title":"J. Formalized Reasoning"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034798"},{"key":"e_1_3_2_1_17_1","unstructured":"Happy 2001. Happy: The parser generator for Haskell. http:\/\/www.haskell.org\/happy.  Happy 2001. Happy: The parser generator for Haskell. http:\/\/www.haskell.org\/happy."},{"volume-title":"Mathematics of Program Construction, Ralf Hinze and Janis Voigtl\u00e4nder (Eds.)","author":"Kokke Pepijn","key":"e_1_3_2_1_18_1","unstructured":"Pepijn Kokke and Wouter Swierstra . 2015. Auto in Agda . In Mathematics of Program Construction, Ralf Hinze and Janis Voigtl\u00e4nder (Eds.) . Springer International Publishing , Cham , 276--301. Pepijn Kokke and Wouter Swierstra. 2015. Auto in Agda. In Mathematics of Program Construction, Ralf Hinze and Janis Voigtl\u00e4nder (Eds.). Springer International Publishing, Cham, 276--301."},{"key":"e_1_3_2_1_19_1","volume-title":"Twenty-five years of constructive type theory (Venice","author":"Martin-L\u00f6f Per","year":"1995","unstructured":"Per Martin-L\u00f6f . 1998. An intuitionistic theory of types . In Twenty-five years of constructive type theory (Venice , 1995 ). Oxford Logic Guides, Vol . 36. Oxford Univ. Press , New York, 127--172. Per Martin-L\u00f6f. 1998. An intuitionistic theory of types. In Twenty-five years of constructive type theory (Venice, 1995). Oxford Logic Guides, Vol. 36. Oxford Univ. Press, New York, 127--172."},{"key":"e_1_3_2_1_20_1","volume-title":"Propositional Proof Systems. Archive of Formal Proofs (June","author":"Michaelis Julius","year":"2017","unstructured":"Julius Michaelis and Tobias Nipkow . 2017. Propositional Proof Systems. Archive of Formal Proofs (June 2017 ). http:\/\/isa-afp.org\/entries\/Propositional_Proof_Systems.html, Formal proof development. Julius Michaelis and Tobias Nipkow. 2017. Propositional Proof Systems. Archive of Formal Proofs (June 2017). http:\/\/isa-afp.org\/entries\/Propositional_Proof_Systems.html, Formal proof development."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006277616879"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/646523.694563"},{"volume-title":"Structural Proof Theory","author":"Negri Sara","key":"e_1_3_2_1_24_1","unstructured":"Sara Negri , Jan von Plato , and Aarne Ranta . 2001. Structural Proof Theory . Cambridge University Press . https:\/\/doi.org\/10.1017\/CBO9780511527340 10.1017\/CBO9780511527340 Sara Negri, Jan von Plato, and Aarne Ranta. 2001. Structural Proof Theory. Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9780511527340"},{"key":"e_1_3_2_1_25_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjoberg, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2018","unstructured":"Benjamin C. Pierce , Arthur Azevedo de Amorim , Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjoberg, and Brent Yorgey. 2018 . Logical Foundations. Electronic textbook. Version 5.5. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjoberg, and Brent Yorgey. 2018. Logical Foundations. Electronic textbook. Version 5.5. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3125374.3125381"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_10"},{"key":"e_1_3_2_1_28_1","unstructured":"Felipe Sasdelli Maycon Amaro Elton Carsodo Samuel Feitosa and Rodrigo Ribeiro. 2020. Proofs of Consistency for Propositional Logic Verified in Coq and Agda. Avaliable at https:\/\/github.com\/lives-group\/consistency.  Felipe Sasdelli Maycon Amaro Elton Carsodo Samuel Feitosa and Rodrigo Ribeiro. 2020. Proofs of Consistency for Propositional Logic Verified in Coq and Agda. Avaliable at https:\/\/github.com\/lives-group\/consistency."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1197021"},{"volume-title":"From Semantics to Computer Science. Essays in Honour of Gilles Kahn, G. Huet, J.-J","author":"Urban Christian","key":"e_1_3_2_1_30_1","unstructured":"Christian Urban and Tobias Nipkow . 2009. Nominal verification of algorithm W . In From Semantics to Computer Science. Essays in Honour of Gilles Kahn, G. Huet, J.-J . Levy, and G. Plotkin (Eds.). Cambridge University Press , 363--382. Christian Urban and Tobias Nipkow. 2009. Nominal verification of algorithm W. In From Semantics to Computer Science. Essays in Honour of Gilles Kahn, G. Huet, J.-J. Levy, and G. Plotkin (Eds.). Cambridge University Press, 363--382."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80046-8"},{"key":"e_1_3_2_1_32_1","unstructured":"Floris van Doorn. 2015. Propositional Calculus in Coq. arXiv:math.LO\/1503.08744  Floris van Doorn. 2015. Propositional Calculus in Coq. arXiv:math.LO\/1503.08744"},{"key":"e_1_3_2_1_33_1","unstructured":"Philip Wadler and Wen Kokke. 2019. Programming Language Foundations in Agda. Available at http:\/\/plfa.inf.ed.ac.uk\/.  Philip Wadler and Wen Kokke. 2019. Programming Language Foundations in Agda. Available at http:\/\/plfa.inf.ed.ac.uk\/."},{"key":"e_1_3_2_1_34_1","volume-title":"12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA","author":"Xavier Bruno","year":"2017","unstructured":"Bruno Xavier , Carlos Olarte , Giselle Reis , and Vivek Nigam . 2017. Mechanizing Focused Linear Logic in Coq . In 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017 , Bras\u00edlia, Brazil, September 23--24, 2017 (Electronic Notes in Theoretical Computer Science), Sandra Alves and Renata Wasserman (Eds.), Vol. 338 . Elsevier , 219--236. https:\/\/doi.org\/10.1016\/j.entcs.2018.10.014 10.1016\/j.entcs.2018.10.014 Bruno Xavier, Carlos Olarte, Giselle Reis, and Vivek Nigam. 2017. Mechanizing Focused Linear Logic in Coq. In 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Bras\u00edlia, Brazil, September 23--24, 2017 (Electronic Notes in Theoretical Computer Science), Sandra Alves and Renata Wasserman (Eds.), Vol. 338. Elsevier, 219--236. https:\/\/doi.org\/10.1016\/j.entcs.2018.10.014"}],"event":{"name":"SBLP '20: 24th Brazilian Symposium on Programming Languages","sponsor":["SBC Brazilian Computer Society"],"location":"Natal Brazil","acronym":"SBLP '20"},"container-title":["Proceedings of the 24th Brazilian Symposium on Context-Oriented Programming and Advanced Modularity"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427081.3427083","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3427081.3427083","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:24Z","timestamp":1750197744000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427081.3427083"}},"subtitle":["Comparing Consistency Proofs for Minimal Propositional Logics"],"short-title":[],"issued":{"date-parts":[[2020,10,19]]},"references-count":34,"alternative-id":["10.1145\/3427081.3427083","10.1145\/3427081"],"URL":"https:\/\/doi.org\/10.1145\/3427081.3427083","relation":{},"subject":[],"published":{"date-parts":[[2020,10,19]]},"assertion":[{"value":"2020-10-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}