Stop the war!
Остановите войну!
for scientists:
default search action
Search dblp for Publications
export results for "toc:db/conf/cpp/cpp2021.bht:"
@inproceedings{DBLP:conf/cpp/AnnenkovMNS21, author = {Danil Annenkov and Mikkel Milo and Jakob Botsch Nielsen and Bas Spitters}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Extracting smart contracts tested and verified in Coq}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {105--121}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439934}, doi = {10.1145/3437992.3439934}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cpp/AnnenkovMNS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/BeckerBGDM21, author = {Heiko Becker and Nathaniel Bos and Ivan Gavran and Eva Darulova and Rupak Majumdar}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Lassie: {HOL4} tactics by example}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {212--223}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439925}, doi = {10.1145/3437992.3439925}, timestamp = {Sat, 09 Apr 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cpp/BeckerBGDM21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/BegayCM21, author = {Pierre{-}L{\'{e}}o B{\'{e}}gay and Pierre Cr{\'{e}}gut and Jean{-}Fran{\c{c}}ois Monin}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Developing and certifying Datalog optimizations in coq/mathcomp}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {163--177}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439913}, doi = {10.1145/3437992.3439913}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/BegayCM21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/BenzakenCCKZ21, author = {V{\'{e}}ronique Benzaken and Sarah Cohen{-}Boulakia and Evelyne Contejean and Chantal Keller and R{\'{e}}becca Zucchini}, editor = {Catalin Hritcu and Andrei Popescu}, title = {A Coq formalization of data provenance}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {152--162}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439920}, doi = {10.1145/3437992.3439920}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cpp/BenzakenCCKZ21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/CattN21, author = {Elliot Catt and Michael Norrish}, editor = {Catalin Hritcu and Andrei Popescu}, title = {On the formalisation of Kolmogorov complexity}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {291--299}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439921}, doi = {10.1145/3437992.3439921}, timestamp = {Fri, 09 Apr 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cpp/CattN21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/ChhakTA21, author = {C. H. R. Chhak and Andrew Tolmach and Sean Noble Anderson}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Towards formally verified compilation of tag-based policy enforcement}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {137--151}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439929}, doi = {10.1145/3437992.3439929}, timestamp = {Mon, 04 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cpp/ChhakTA21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/CommelinL21, author = {Johan Commelin and Robert Y. Lewis}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Formalizing the ring of Witt vectors}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {264--277}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439919}, doi = {10.1145/3437992.3439919}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/CommelinL21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/DesharnaisB21, author = {Martin Desharnais and Stefan Brunthaler}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Towards efficient and verified virtual machines for dynamic languages}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {61--75}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439923}, doi = {10.1145/3437992.3439923}, timestamp = {Tue, 07 May 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cpp/DesharnaisB21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/HaslbeckT21, author = {Max W. Haslbeck and Ren{\'{e}} Thiemann}, editor = {Catalin Hritcu and Andrei Popescu}, title = {An Isabelle/HOL formalization of AProVE's termination method for {LLVM} {IR}}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {238--249}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439935}, doi = {10.1145/3437992.3439935}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/HaslbeckT21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/HinrichsenLKB21, author = {Jonas Kastberg Hinrichsen and Dani{\"{e}}l Louwrink and Robbert Krebbers and Jesper Bengtson}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Machine-checked semantic session typing}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {178--198}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439914}, doi = {10.1145/3437992.3439914}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cpp/HinrichsenLKB21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/HuC21, author = {Jason Z. S. Hu and Jacques Carette}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Formalizing category theory in Agda}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {327--342}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439922}, doi = {10.1145/3437992.3439922}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cpp/HuC21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/KirstR21, author = {Dominik Kirst and Felix Rech}, editor = {Catalin Hritcu and Andrei Popescu}, title = {The generalised continuum hypothesis implies the axiom of choice in Coq}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {313--326}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439932}, doi = {10.1145/3437992.3439932}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/KirstR21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/Laurent21, author = {Olivier Laurent}, editor = {Catalin Hritcu and Andrei Popescu}, title = {An anti-locally-nameless approach to formalizing quantifiers}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {300--312}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439926}, doi = {10.1145/3437992.3439926}, timestamp = {Mon, 06 Nov 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/Laurent21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/Limperg21, author = {Jannis Limperg}, editor = {Catalin Hritcu and Andrei Popescu}, title = {A novice-friendly induction tactic for lean}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {199--211}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439928}, doi = {10.1145/3437992.3439928}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/Limperg21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/LochmannMMF21, author = {Alexander Lochmann and Aart Middeldorp and Fabian Mitterwallner and Bertram Felgenhauer}, editor = {Catalin Hritcu and Andrei Popescu}, title = {A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {250--263}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439918}, doi = {10.1145/3437992.3439918}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/LochmannMMF21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/Loow21, author = {Andreas L{\"{o}}{\"{o}}w}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Lutsig: a verified Verilog compiler for verified circuit development}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {46--60}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439916}, doi = {10.1145/3437992.3439916}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/Loow21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/MiraldoCMSS21, author = {Victor Cacciari Miraldo and Harold Carr and Mark Moir and Lisandra Silva and Guy L. Steele Jr.}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Formal verification of authenticated, append-only skip lists in Agda}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {122--136}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439924}, doi = {10.1145/3437992.3439924}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/MiraldoCMSS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/Myreen21, author = {Magnus O. Myreen}, editor = {Catalin Hritcu and Andrei Popescu}, title = {A minimalistic verified bootstrapped compiler (proof pearl)}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {32--45}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439915}, doi = {10.1145/3437992.3439915}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/Myreen21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/Nipkow21, author = {Tobias Nipkow}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Teaching algorithms and data structures with a proof assistant (invited talk)}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {1--3}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439910}, doi = {10.1145/3437992.3439910}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/Nipkow21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/Sewell21, author = {Peter Sewell}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk)}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {4}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439911}, doi = {10.1145/3437992.3439911}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/Sewell21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/SlagelWD21, author = {J. Tanner Slagel and Lauren M. White and Aaron Dutle}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Formal verification of semi-algebraic sets and real analytic functions}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {278--290}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439933}, doi = {10.1145/3437992.3439933}, timestamp = {Mon, 03 Jun 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/cpp/SlagelWD21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/TassarottiV0T21, author = {Joseph Tassarotti and Koundinya Vajjha and Anindya Banerjee and Jean{-}Baptiste Tristan}, editor = {Catalin Hritcu and Andrei Popescu}, title = {A formal proof of {PAC} learnability for decision stumps}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {5--17}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439917}, doi = {10.1145/3437992.3439917}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/TassarottiV0T21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/TimanyB21, author = {Amin Timany and Lars Birkedal}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Reasoning about monotonicity in separation logic}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {91--104}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439931}, doi = {10.1145/3437992.3439931}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/TimanyB21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/TourretB21, author = {Sophie Tourret and Jasmin Blanchette}, editor = {Catalin Hritcu and Andrei Popescu}, title = {A modular Isabelle framework for verifying saturation provers}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {224--237}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439912}, doi = {10.1145/3437992.3439912}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/TourretB21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/VajjhaSTPF21, author = {Koundinya Vajjha and Avraham Shinnar and Barry M. Trager and Vasily Pestun and Nathan Fulton}, editor = {Catalin Hritcu and Andrei Popescu}, title = {CertRL: formalizing convergence proofs for value and policy iteration in Coq}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {18--31}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439927}, doi = {10.1145/3437992.3439927}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/VajjhaSTPF21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/cpp/VindumB21, author = {Simon Friis Vindum and Lars Birkedal}, editor = {Catalin Hritcu and Andrei Popescu}, title = {Contextual refinement of the Michael-Scott queue (proof pearl)}, booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, pages = {76--90}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992.3439930}, doi = {10.1145/3437992.3439930}, timestamp = {Sat, 08 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/VindumB21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/cpp/2021, editor = {Catalin Hritcu and Andrei Popescu}, title = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3437992}, doi = {10.1145/3437992}, isbn = {978-1-4503-8299-1}, timestamp = {Fri, 12 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/cpp/2021.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.