default search action

combined dblp search
author search
venue search
publication search

ask others

9th CPP 2020: New Orleans, LA, USA

> 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/2020
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2020
Jasmin Blanchette, Catalin Hritcu:
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. ACM 2020, ISBN 978-1-4503-7097-4
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Rosu020
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Rosu020
Grigore Rosu, Xiaohong Chen:
Matching logic: the foundation of the K framework (invited talk). 1
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Chlipala20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Chlipala20
Adam Chlipala:
Proof assistants at the hardware-software interface (invited talk). 2
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BlaudeauS20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BlaudeauS20
Clement Blaudeau, Natarajan Shankar:
A verified packrat parser interpreter for parsing expression grammars. 3-17
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/NipkowS20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/NipkowS20
Tobias Nipkow, Thomas Sewell:
Proof pearl: Braun trees. 18-31
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LetanR20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LetanR20
Thomas Letan, Yann Régis-Gianas:
FreeSpec: specifying, verifying, and executing impure computations in Coq. 32-46
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/GoelSSS20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/GoelSSS20
Shilpi Goel, Anna Slobodová, Rob Sumners, Sol Swords:
Verifying x86 instruction implementations. 47-60
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AltmanningerP20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AltmanningerP20
Johannes Altmanninger, Adrian Rebola-Pardo:
Frying the egg, roasting the chicken: unit deletions in DRAT proofs. 61-70
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ZakowskiHHZ20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ZakowskiHHZ20
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic:
An equational theory for weak bisimulation via generalized parameterized coinduction. 71-84
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/WangBKU20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/WangBKU20
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban:
Exploration of neural machine translation in autoformalization of mathematics in Mizar. 85-98
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/RingerSGL20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/RingerSGL20
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner:
REPLica: REPL instrumentation for Coq analysis. 99-113
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/0002KW20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/0002KW20
Yannick Forster, Fabian Kunze, Maxi Wuttke:
Verified programming of Turing machines in Coq. 114-128
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/TranMH20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/TranMH20
Linh Tran, Anshuman Mohan, Aquinas Hobor:
A functional proof pearl: inverting the Ackermann hierarchy. 129-142
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Spies020
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Spies020
Simon Spies, Yannick Forster:
Undecidability of higher-order unification formalised in Coq. 143-157
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/MortbergP20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/MortbergP20
Anders Mörtberg, Loïc Pujet:
Cubical synthetic homotopy theory. 158-171
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ForsbergXG20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ForsbergXG20
Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani:
Three equivalent ordinal notation systems in cubical Agda. 172-185
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/0002S20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/0002S20
Yannick Forster, Kathrin Stark:
Coq à la carte: a practical approach to modular syntax with binders. 186-200
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DiazOT20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DiazOT20
Tomás Díaz, Federico Olmedo, Éric Tanter:
A mechanized formalization of GraphQL. 201-214
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AnnenkovNS20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AnnenkovNS20
Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters:
ConCert: a smart contract certification framework in Coq. 215-228
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/00020G20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/00020G20
David Butler, David Aspinall, Adrià Gascón:
Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. 229-243
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FirsovBTL20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FirsovBTL20
Denis Firsov, Ahto Buldas, Ahto Truu, Risto Laanoja:
Verified security of BLT signature scheme. 244-257
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Overbeek20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Overbeek20
Roy Overbeek:
Formalizing determinacy of concurrent revisions. 258-269
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/VeltriV20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/VeltriV20
Niccolò Veltri, Andrea Vezzosi:
Formalizing π-calculus in guarded cubical Agda. 270-283
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/RouvoetPKV20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/RouvoetPKV20
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser:
Intrinsically-typed definitional interpreters for linear, session-typed languages. 284-298
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BuzzardCM20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BuzzardCM20
Kevin Buzzard, Johan Commelin, Patrick Massot:
Formalising perfectoid spaces. 299-312
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/SinghN20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/SinghN20
Abhishek Kr Singh, Raja Natarajan:
A constructive formalization of the weak perfect graph theorem. 313-324
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DoczkalP20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DoczkalP20
Christian Doczkal, Damien Pous:
Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. 325-337
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ImmlerT20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ImmlerT20
Fabian Immler, Yong Kiam Tan:
The Poincaré-Bendixson theorem in Isabelle/HOL. 338-352
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HanD20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HanD20
Jesse Michael Han, Floris van Doorn:
A formal proof of the independence of the continuum hypothesis. 353-366
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/X20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/X20
The lean mathematical library. 367-381

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.