{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:29Z","timestamp":1767927989863,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":92,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"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":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294087","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Formalizing the metatheory of logical calculi and automatic provers in Isabelle\/HOL (invited talk)"],"prefix":"10.1145","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[{"name":"Vrije Universiteit Amsterdam, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"399","volume-title":"Predicting Learnt Clauses Quality in Modern SAT Solvers. In IJCAI","author":"Audemard Gilles","year":"2009"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Franz Baader and Tobias Nipkow. 1998. Term Rewriting and All That. Cambridge University Press.   Franz Baader and Tobias Nipkow. 1998. Term Rewriting and All That . Cambridge University Press.","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_3_2_1_3_1","volume-title":"Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.).","author":"Bachmair Leo"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9284-7"},{"key":"e_1_3_2_1_5_1","unstructured":"Bruno Barras. 1999. Auto-validation d'un syst\u00e8me de preuves avec familles inductives. Ph.D. Dissertation. Universit\u00e9 Paris 7.  Bruno Barras. 1999. Auto-validation d'un syst\u00e8me de preuves avec familles inductives . Ph.D. Dissertation. Universit\u00e9 Paris 7."},{"key":"e_1_3_2_1_6_1","first-page":"432","volume-title":"LNCS","volume":"10395","author":"Becker Heiko","year":"2017"},{"key":"e_1_3_2_1_7_1","unstructured":"Alexander Bentkamp. 2018. Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms. Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/Lambda_Free_EPO.html.  Alexander Bentkamp. 2018. Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms. Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/Lambda_Free_EPO.html."},{"key":"e_1_3_2_1_8_1","first-page":"28","volume-title":"Superposition for Lambda-Free Higher-Order Logic. In IJCAR","volume":"10900","author":"Bentkamp Alexander","year":"2018"},{"key":"e_1_3_2_1_9_1","unstructured":"Stefan Berghofer. 2007. First-Order Logic According to Fitting. Archive of Formal Proofs (2007). http:\/\/isa-afp.org\/entries\/FOL-Fitting.html.  Stefan Berghofer. 2007. First-Order Logic According to Fitting. Archive of Formal Proofs (2007). http:\/\/isa-afp.org\/entries\/FOL-Fitting.html."},{"key":"e_1_3_2_1_10_1","first-page":"3","volume-title":"LNCS","volume":"10483","author":"Biendarra Julian","year":"2017"},{"key":"e_1_3_2_1_11_1","unstructured":"Armin Biere. 2017. CaDiCaL Lingeling Plingeling Treengeling YalSAT Entering the SAT Competition 2017. In SAT Competition 2017: Solver and Benchmark Descriptions Tom\u00e1? Balyo Marijn Heule and Matti J\u00e4rvisalo (Eds.). University of Helsinki 14-15.  Armin Biere. 2017. CaDiCaL Lingeling Plingeling Treengeling YalSAT Entering the SAT Competition 2017. In SAT Competition 2017: Solver and Benchmark Descriptions Tom\u00e1? Balyo Marijn Heule and Matti J\u00e4rvisalo (Eds.). University of Helsinki 14-15."},{"key":"e_1_3_2_1_12_1","first-page":"39","volume-title":"AVATAR Modulo Theories. In GCAI","volume":"41","author":"Nikolaj","year":"2016"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9455-7"},{"key":"e_1_3_2_1_14_1","volume-title":"FSCD","volume":"84","author":"Blanchette Jasmin Christian","year":"2017"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_4"},{"key":"e_1_3_2_1_16_1","volume-title":"Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In ITP","author":"Blanchette Jasmin Christian","year":"2010"},{"key":"e_1_3_2_1_17_1","volume-title":"FroCoS","author":"Blanchette Jasmin Christian","year":"2013"},{"key":"e_1_3_2_1_18_1","unstructured":"Jasmin Christian Blanchette and Andrei Popescu. 2013. Sound and Complete Sort Encodings for First-Order Logic. Archive of Formal Proofs (2013). http:\/\/isa-afp.org\/entries\/Sort_Encodings.html.  Jasmin Christian Blanchette and Andrei Popescu. 2013. Sound and Complete Sort Encodings for First-Order Logic. Archive of Formal Proofs (2013). http:\/\/isa-afp.org\/entries\/Sort_Encodings.html."},{"key":"e_1_3_2_1_19_1","unstructured":"Jasmin Christian Blanchette Andrei Popescu and Dmitriy Traytel. 2017. Abstract Completeness. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Abstract_Completeness.html.  Jasmin Christian Blanchette Andrei Popescu and Dmitriy Traytel. 2017. Abstract Completeness. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Abstract_Completeness.html."},{"key":"e_1_3_2_1_20_1","unstructured":"Jasmin Christian Blanchette Andrei Popescu and Dmitriy Traytel. 2017. Abstract Soundness. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Abstract_Soundness.html.  Jasmin Christian Blanchette Andrei Popescu and Dmitriy Traytel. 2017. Abstract Soundness. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Abstract_Soundness.html."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9391-3"},{"key":"e_1_3_2_1_22_1","volume-title":"FoSSaCS","author":"Blanchette Jasmin Christian","year":"2017"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000120"},{"key":"e_1_3_2_1_24_1","volume-title":"CADE-26, Leonardo de Moura (Ed.). LNCS","author":"Brockschmidt Marc"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"e_1_3_2_1_26_1","volume-title":"TPHOLs","author":"Bulwahn Lukas","year":"2008"},{"key":"e_1_3_2_1_27_1","volume-title":"RTA '11","volume":"10","author":"Contejean \u00c9velyne","year":"2011"},{"key":"e_1_3_2_1_28_1","volume-title":"CADE-26, Leonardo de Moura (Ed.). LNCS","author":"Cruz-Filipe Lu\u00eds"},{"key":"e_1_3_2_1_29_1","unstructured":"Jared C. Davis. 2009. A Self-Verifying Theorem Prover. Ph.D. Dissertation. University of Texas at Austin.   Jared C. Davis. 2009. A Self-Verifying Theorem Prover . Ph.D. Dissertation. University of Texas at Austin."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/359138.359142"},{"key":"e_1_3_2_1_31_1","first-page":"502","volume-title":"An Extensible SAT-Solver. In SAT","volume":"2919","author":"E\u00e9n Niklas","year":"2003"},{"key":"e_1_3_2_1_32_1","first-page":"1","article-title":"Labelled","volume":"55","author":"Fietzke Arnaud","year":"2009","journal-title":"Splitting. Ann. Math. Artif. Intell."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1145\/3167080","volume-title":"CPP","author":"Fleury Mathias","year":"2018"},{"key":"e_1_3_2_1_34_1","unstructured":"Andreas Halkj\u00e6r From. 2017. First-Order Logic According to Berghofer. Isabelle Formalization of Logic (2017). https:\/\/bitbucket.org\/isafol\/isafol\/src\/master\/FOL_Berghofer\/.  Andreas Halkj\u00e6r From. 2017. First-Order Logic According to Berghofer. Isabelle Formalization of Logic (2017). https:\/\/bitbucket.org\/isafol\/isafol\/src\/master\/FOL_Berghofer\/."},{"key":"e_1_3_2_1_35_1","unstructured":"Andreas Halkj\u00e6r From. 2018. Epistemic Logic. Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/Epistemic_Logic.shtml.  Andreas Halkj\u00e6r From. 2018. Epistemic Logic. Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/Epistemic_Logic.shtml."},{"key":"e_1_3_2_1_36_1","volume-title":"Substitutionless First-Order Logic: A Formal Soundness Proof. In Isabelle Workshop","author":"From Andreas Halkj\u00e6r","year":"2018"},{"key":"e_1_3_2_1_37_1","volume-title":"Proof, Language, and Interaction, Essays in Honour of Robin Milner, Gordon D","author":"Gordon Mike"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"e_1_3_2_1_39_1","first-page":"153","volume-title":"Formalizing Basic First Order Model Theory. In TPHOLs '98","volume":"1479","author":"Harrison John","year":"1998"},{"key":"e_1_3_2_1_40_1","first-page":"177","volume-title":"Towards Self-Verification of HOL Light. In IJCAR","volume":"4130","author":"Harrison John","year":"2006"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press.   John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning . Cambridge University Press.","DOI":"10.1017\/CBO9780511576430"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1549"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"crossref","unstructured":"G\u00e9rard Huet and Derek C. Oppen. 1980. Equations and Rewrite Rules: A Survey. In Formal Language Theory: Perspectives and Open Problems R. V. Book (Ed.). Academic Press 349-405.  G\u00e9rard Huet and Derek C. Oppen. 1980. Equations and Rewrite Rules: A Survey. In Formal Language Theory: Perspectives and Open Problems R. V. Book (Ed.). Academic Press 349-405.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"e_1_3_2_1_44_1","first-page":"131","volume-title":"Lifting and Transfer: A Modular Design for Quotients in Isabelle\/HOL. In CPP","volume":"8307","author":"Huffman Brian","year":"2013"},{"key":"e_1_3_2_1_46_1","first-page":"355","volume-title":"Inprocessing Rules. In IJCAR","volume":"7364","author":"J\u00e4rvisalo Matti","year":"2012"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-180764"},{"key":"e_1_3_2_1_48_1","unstructured":"Alexander Birch Jensen Anders Schlichtkrull and J\u00f8rgen Villadsen. 2017. First-Order Logic According to Harrison. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/FOL_Harrison.html.  Alexander Birch Jensen Anders Schlichtkrull and J\u00f8rgen Villadsen. 2017. First-Order Logic According to Harrison. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/FOL_Harrison.html."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.43.1"},{"key":"e_1_3_2_1_50_1","volume-title":"FroCoS","author":"Krstic Sava","year":"2007"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9357-x"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_53_1","volume-title":"ITP","author":"Lammich Peter","year":"2013"},{"key":"e_1_3_2_1_54_1","volume-title":"ITP","author":"Lammich Peter","year":"2015"},{"key":"e_1_3_2_1_55_1","volume-title":"CADE-26, Leonardo de Moura (Ed.). LNCS","author":"Lammich Peter"},{"key":"e_1_3_2_1_56_1","first-page":"457","volume-title":"The GRAT Tool Chain--Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees. In SAT","volume":"10491","author":"Lammich Peter","year":"2017"},{"key":"e_1_3_2_1_57_1","first-page":"453","volume-title":"Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. In SAT","volume":"5584","author":"Larrosa Javier","year":"2009"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9176-z"},{"key":"e_1_3_2_1_59_1","unstructured":"Stephane Lescuyer. 2011. Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. Ph.D. Dissertation. Universit\u00e9 Paris-Sud.  Stephane Lescuyer. 2011. Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq . Ph.D. Dissertation. Universit\u00e9 Paris-Sud."},{"key":"e_1_3_2_1_60_1","unstructured":"Filip Maric. 2008. Formal Verification of Modern SAT Solvers. Archive of Formal Proofs (2008). http:\/\/isa-afp.org\/entries\/SATSolverVerification.html.  Filip Maric. 2008. Formal Verification of Modern SAT Solvers. Archive of Formal Proofs (2008). http:\/\/isa-afp.org\/entries\/SATSolverVerification.html."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.014"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"crossref","unstructured":"Filip Maric and Predrag Janicic. 2011. Formalization of Abstract State Transition Systems for SAT. Log. Meth. Comput. Sci. 7 3 (2011).  Filip Maric and Predrag Janicic. 2011. Formalization of Abstract State Transition Systems for SAT. Log. Meth. Comput. Sci. 7 3 (2011).","DOI":"10.2168\/LMCS-7(3:19)2011"},{"key":"e_1_3_2_1_63_1","unstructured":"Filip Maric Mirko Spasic and Ren\u00e9 Thiemann. 2018. An Incremental Simplex Algorithm with Unsatisfiable Core Generation. Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/Simplex.shtml.  Filip Maric Mirko Spasic and Ren\u00e9 Thiemann. 2018. An Incremental Simplex Algorithm with Unsatisfiable Core Generation. Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/Simplex.shtml."},{"key":"e_1_3_2_1_64_1","unstructured":"Julius Michaelis and Tobias Nipkow. 2017. Proof Systems for Propositional Logic. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Propositional_Proof_Systems.html.  Julius Michaelis and Tobias Nipkow. 2017. Proof Systems for Propositional Logic. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Propositional_Proof_Systems.html."},{"key":"e_1_3_2_1_65_1","volume-title":"Formalized Proof Systems for Propositional Logic. In TYPES","volume":"104","author":"Michaelis Julius","year":"2018"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_67_1","first-page":"265","volume-title":"ITP","volume":"6898","author":"Magnus","year":"2011"},{"key":"e_1_3_2_1_68_1","first-page":"421","volume-title":"ITP","volume":"8558","author":"Magnus","year":"2014"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_3"},{"key":"e_1_3_2_1_71_1","volume-title":"TPHOLs","author":"O'Connor Russell","year":"2005"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_24"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_5"},{"key":"e_1_3_2_1_74_1","unstructured":"Lawrence C. Paulson. 2013. G\u00f6del's Incompleteness Theorems. Archive of Formal Proofs (2013). http:\/\/isa-afp.org\/entries\/Incompleteness.html.  Lawrence C. Paulson. 2013. G\u00f6del's Incompleteness Theorems. Archive of Formal Proofs (2013). http:\/\/isa-afp.org\/entries\/Incompleteness.html."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9322-8"},{"key":"e_1_3_2_1_76_1","first-page":"1","article-title":"Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In IWIL-2010, Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska (Eds.). EPiC Series in Computing, Vol. 2","author":"Paulson Lawrence C.","year":"2012","journal-title":"EasyChair"},{"key":"e_1_3_2_1_77_1","unstructured":"Nicolas Peltier. 2016. Propositional Resolution and Prime Implicates Generation. Archive of Formal Proofs (2016). http:\/\/www.isa-afp.org\/entries\/PropResPI.html.  Nicolas Peltier. 2016. Propositional Resolution and Prime Implicates Generation. Archive of Formal Proofs (2016). http:\/\/www.isa-afp.org\/entries\/PropResPI.html."},{"key":"e_1_3_2_1_78_1","unstructured":"Nicolas Peltier. 2016. A Variant of the Superposition Calculus. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/SuperCalc.html.  Nicolas Peltier. 2016. A Variant of the Superposition Calculus. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/SuperCalc.html."},{"key":"e_1_3_2_1_79_1","unstructured":"Henrik Persson. 1996. Constructive Completeness of Intuitionistic Predicate Logic: A Formalisation in Type Theory. Licentiate Thesis. Chalmers tekniska h\u00f6gskola and G\u00f6teborgs universitet.  Henrik Persson. 1996. Constructive Completeness of Intuitionistic Predicate Logic: A Formalisation in Type Theory . Licentiate Thesis. Chalmers tekniska h\u00f6gskola and G\u00f6teborgs universitet."},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596552"},{"key":"e_1_3_2_1_81_1","volume-title":"CADE-25, Amy P","author":"Reger Giles"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"crossref","unstructured":"Tom Ridge. 2004. A Mechanically Verified Efficient Sound and Complete Theorem Prover For First Order Logic. Archive of Formal Proofs (2004). http:\/\/isa-afp.org\/entries\/Verified-Prover.shtml.  Tom Ridge. 2004. A Mechanically Verified Efficient Sound and Complete Theorem Prover For First Order Logic. Archive of Formal Proofs (2004). http:\/\/isa-afp.org\/entries\/Verified-Prover.shtml.","DOI":"10.1007\/11541868_19"},{"key":"e_1_3_2_1_83_1","volume-title":"TPHOLs","author":"Ridge Tom","year":"2005"},{"key":"e_1_3_2_1_84_1","unstructured":"Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier and MIT Press. Vols. I and II.  Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning . Elsevier and MIT Press. Vols. I and II."},{"key":"e_1_3_2_1_85_1","volume-title":"Haskell","author":"Runciman Colin","year":"2008"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"crossref","unstructured":"Anders Schlichtkrull. 2016. The Resolution Calculus for First-Order Logic. Archive of Formal Proofs (2016). http:\/\/www.isa-afp.org\/entries\/Resolution_FOL.html.  Anders Schlichtkrull. 2016. The Resolution Calculus for First-Order Logic. Archive of Formal Proofs (2016). http:\/\/www.isa-afp.org\/entries\/Resolution_FOL.html.","DOI":"10.1007\/978-3-319-43144-4_21"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9447-z"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294100"},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.29007\/pn71"},{"key":"e_1_3_2_1_90_1","unstructured":"Anders Schlichtkrull and J\u00f8rgen Villadsen. 2016. Paraconsistency. Archive of Formal Proofs (2016). http:\/\/www.isa-afp.org\/entries\/Paraconsistency.html.  Anders Schlichtkrull and J\u00f8rgen Villadsen. 2016. Paraconsistency. Archive of Formal Proofs (2016). http:\/\/www.isa-afp.org\/entries\/Paraconsistency.html."},{"key":"e_1_3_2_1_91_1","first-page":"2","article-title":"E--a Brainiac Theorem Prover","volume":"15","author":"Schulz Stephan","year":"2002","journal-title":"AI Commun."},{"key":"e_1_3_2_1_92_1","first-page":"477","volume-title":"Fingerprint Indexing for Paramodulation and Rewriting. In IJCAR","volume":"7364","author":"Schulz Stephan","year":"2012"},{"key":"e_1_3_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.5555\/261782"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Cascais Portugal","acronym":"CPP '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294087","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294087","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:49Z","timestamp":1750207429000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294087"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":92,"alternative-id":["10.1145\/3293880.3294087","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294087","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}