default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID7. CPP 2018: Los Angeles, CA, USA
- June Andronick, Amy P. Felty:
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018. ACM 2018, ISBN 978-1-4503-5586-5
Invited Talks
- Brigitte Pientka:
POPLMark reloaded: mechanizing logical relations proofs (invited talk). 1 - Jose Divasón
, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada:
Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). 2-13
Verifing Programs and Systems
- Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich:
Total Haskell is reasonable Coq. 14-27 - Damien Rouhling:
A formal proof in Coq of a control function for the inverted pendulum. 28-41 - Christian Doczkal, Joachim Bard:
Completeness and decidability of converse PDL in the constructive type theory of Coq. 42-52
Verified Applications
- Conrad Watt:
Mechanising and verifying the WebAssembly specification. 53-65 - Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples:
Towards verifying ethereum smart contract bytecode in Isabelle/HOL. 66-77 - George Pîrlea, Ilya Sergey:
Mechanising blockchain consensus. 78-90 - Cezary Kaliszyk, Julian Parsert:
Formal microeconomic foundations and the first welfare theorem. 91-101
Proof Methods and Libraries
- Craig McLaughlin, James McKinna, Ian Stark:
Triangulating context lemmas. 102-114 - Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman:
Adapting proof automation to adapt proofs. 115-129 - Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin:
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. 130-145 - Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak:
Formal proof of polynomial-time complexity with quasi-interpretations. 146-157
Trusted Verification Frameworks and Systems
- Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich:
A verified SAT solver with watched literals using imperative HOL. 158-171 - Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman:
Œuf: minimizing the Coq extraction TCB. 172-185 - Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Proofs in conflict-driven theory combination. 186-200
Type Theory, Set Theory, and Formalized Mathematics
- Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide:
Finite sets in homotopy type theory. 201-214 - Denis Firsov, Aaron Stump:
Generic derivation of induction for impredicative encodings in Cedille. 215-227 - Dominik Kirst, Gert Smolka:
Large model constructions for second-order ZF in dependent type theory. 228-239 - Boris Djalal:
A constructive formalisation of Semi-algebraic sets and functions. 240-251
Formalizing Meta-Theory
- Sergueï Lenglet, Alan Schmitt:
HOπ in Coq. 252-265 - Pawel Wieczorek, Dariusz Biernacki:
A Coq formalization of normalization by evaluation for Martin-Löf type theory. 266-279 - Kaustuv Chaudhuri:
A two-level logic perspective on (simultaneous) substitutions. 280-292 - Jonas Kaiser, Steven Schäfer, Kathrin Stark:
Binder aware recursion over well-scoped de Bruijn syntax. 293-306
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:
