default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID10th CPP 2021: Virtual Event, Denmark
- Catalin Hritcu, Andrei Popescu:
CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021. ACM 2021, ISBN 978-1-4503-8299-1 - Tobias Nipkow
:
Teaching algorithms and data structures with a proof assistant (invited talk). 1-3 - Peter Sewell:
Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk). 4 - Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan:
A formal proof of PAC learnability for decision stumps. 5-17 - Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton:
CertRL: formalizing convergence proofs for value and policy iteration in Coq. 18-31 - Magnus O. Myreen:
A minimalistic verified bootstrapped compiler (proof pearl). 32-45 - Andreas Lööw:
Lutsig: a verified Verilog compiler for verified circuit development. 46-60 - Martin Desharnais, Stefan Brunthaler:
Towards efficient and verified virtual machines for dynamic languages. 61-75 - Simon Friis Vindum, Lars Birkedal:
Contextual refinement of the Michael-Scott queue (proof pearl). 76-90 - Amin Timany, Lars Birkedal:
Reasoning about monotonicity in separation logic. 91-104 - Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters:
Extracting smart contracts tested and verified in Coq. 105-121 - Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr.:
Formal verification of authenticated, append-only skip lists in Agda. 122-136 - Chris Chhak, Andrew Tolmach, Sean Noble Anderson:
Towards formally verified compilation of tag-based policy enforcement. 137-151 - Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini:
A Coq formalization of data provenance. 152-162 - Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin:
Developing and certifying Datalog optimizations in coq/mathcomp. 163-177 - Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson:
Machine-checked semantic session typing. 178-198 - Jannis Limperg:
A novice-friendly induction tactic for lean. 199-211 - Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar:
Lassie: HOL4 tactics by example. 212-223 - Sophie Tourret, Jasmin Blanchette:
A modular Isabelle framework for verifying saturation provers. 224-237 - Max W. Haslbeck, René Thiemann:
An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. 238-249 - Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer:
A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems. 250-263 - Johan Commelin, Robert Y. Lewis:
Formalizing the ring of Witt vectors. 264-277 - J. Tanner Slagel, Lauren M. White, Aaron Dutle:
Formal verification of semi-algebraic sets and real analytic functions. 278-290 - Elliot Catt, Michael Norrish:
On the formalisation of Kolmogorov complexity. 291-299 - Olivier Laurent:
An anti-locally-nameless approach to formalizing quantifiers. 300-312 - Dominik Kirst, Felix Rech:
The generalised continuum hypothesis implies the axiom of choice in Coq. 313-326 - Jason Z. S. Hu, Jacques Carette:
Formalizing category theory in Agda. 327-342
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.
last updated on 2025-12-09 23:25 CET 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:
