Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSearch dblp for Publications
export results for "toc:db/conf/cpp/cpp2021.bht:"
download as .bib file
@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 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 = {Sat, 08 Jan 2022 00:00:00 +0100},
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}
}
a service of 
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.
retrieved on 2024-05-28 06:05 CEST from data curated by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
