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