![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
7. 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
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
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.