default search action

combined dblp search
author search
venue search
publication search

ask others

10th CPP 2021: Virtual Event, Denmark

> Home > Conferences and Workshops > CPP

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/2021
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2021
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
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Nipkow21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Nipkow21
Tobias Nipkow:
Teaching algorithms and data structures with a proof assistant (invited talk). 1-3
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Sewell21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Sewell21
Peter Sewell:
Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk). 4
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/TassarottiV0T21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/TassarottiV0T21
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan:
A formal proof of PAC learnability for decision stumps. 5-17
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/VajjhaSTPF21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/VajjhaSTPF21
Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton:
CertRL: formalizing convergence proofs for value and policy iteration in Coq. 18-31
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Myreen21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Myreen21
Magnus O. Myreen:
A minimalistic verified bootstrapped compiler (proof pearl). 32-45
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Loow21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Loow21
Andreas Lööw:
Lutsig: a verified Verilog compiler for verified circuit development. 46-60
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DesharnaisB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DesharnaisB21
Martin Desharnais, Stefan Brunthaler:
Towards efficient and verified virtual machines for dynamic languages. 61-75
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/VindumB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/VindumB21
Simon Friis Vindum, Lars Birkedal:
Contextual refinement of the Michael-Scott queue (proof pearl). 76-90
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/TimanyB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/TimanyB21
Amin Timany, Lars Birkedal:
Reasoning about monotonicity in separation logic. 91-104
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AnnenkovMNS21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AnnenkovMNS21
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters:
Extracting smart contracts tested and verified in Coq. 105-121
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/MiraldoCMSS21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/MiraldoCMSS21
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
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ChhakTA21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ChhakTA21
Chris Chhak, Andrew Tolmach, Sean Noble Anderson:
Towards formally verified compilation of tag-based policy enforcement. 137-151
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BenzakenCCKZ21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BenzakenCCKZ21
Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini:
A Coq formalization of data provenance. 152-162
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BegayCM21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BegayCM21
Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin:
Developing and certifying Datalog optimizations in coq/mathcomp. 163-177
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HinrichsenLKB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HinrichsenLKB21
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson:
Machine-checked semantic session typing. 178-198
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Limperg21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Limperg21
Jannis Limperg:
A novice-friendly induction tactic for lean. 199-211
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BeckerBGDM21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BeckerBGDM21
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar:
Lassie: HOL4 tactics by example. 212-223
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/TourretB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/TourretB21
Sophie Tourret, Jasmin Blanchette:
A modular Isabelle framework for verifying saturation provers. 224-237
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HaslbeckT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HaslbeckT21
Max W. Haslbeck, René Thiemann:
An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. 238-249
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LochmannMMF21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LochmannMMF21
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
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CommelinL21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CommelinL21
Johan Commelin, Robert Y. Lewis:
Formalizing the ring of Witt vectors. 264-277
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/SlagelWD21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/SlagelWD21
J. Tanner Slagel, Lauren M. White, Aaron Dutle:
Formal verification of semi-algebraic sets and real analytic functions. 278-290
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CattN21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CattN21
Elliot Catt, Michael Norrish:
On the formalisation of Kolmogorov complexity. 291-299
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Laurent21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Laurent21
Olivier Laurent:
An anti-locally-nameless approach to formalizing quantifiers. 300-312
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KirstR21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KirstR21
Dominik Kirst, Felix Rech:
The generalised continuum hypothesis implies the axiom of choice in Coq. 313-326
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HuC21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HuC21
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.