default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID6. CPP 2017: Paris, France
- Yves Bertot, Viktor Vafeiadis:
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. ACM 2017, ISBN 978-1-4503-4705-1
Keynotes
- Lawrence C. Paulson:
Porting the HOL light analysis library: some lessons (invited talk). 1 - Xinyu Feng:
Mechanized verification of preemptive OS kernels (invited talk). 2
Algorithm and Library Verification
- François Pottier
:
Verifying a hash table and its iterators in higher-order separation logic. 3-16 - Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A formalization of the Berlekamp-Zassenhaus factorization algorithm. 17-29 - Reynald Affeldt, Cyril Cohen:
Formal foundations of 3D geometry to model robot manipulators. 30-42
Automated Proof and Its Formal Verification
- Jan Jakubuv, Josef Urban:
BliStrTune: hierarchical invention of theorem proving strategies. 43-52 - Reuben N. S. Rowe, James Brotherston:
Automatic cyclic termination proofs for recursive procedures in separation logic. 53-65 - Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto:
Formalization of Karp-Miller tree construction on petri nets. 66-78
Formalized Mathematics with Numerical Computations
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero:
A Coq formal proof of the LaxMilgram theorem. 79-89 - Érik Martin-Dorel, Pierre Roux:
A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. 90-99 - Johannes Hölzl:
Markov processes in Isabelle/HOL. 100-111 - Gaëtan Gilbert:
Formalising real numbers in homotopy type theory. 112-124
Verified Programming Tools
- Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar:
Verified compilation of CakeML to multiple machine-code targets. 125-137 - Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong:
Complx: a verification framework for concurrent imperative programs. 138-150 - William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti:
Verifying dynamic race detection. 151-163
Homotopy Type Theory
- Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters:
The HoTT library: a formalization of homotopy type theory in Coq. 164-172 - Jesper Cockx, Dominique Devriese:
Lifting proof-relevant unification to higher dimensions. 173-181 - Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau:
The next 700 syntactical models of type theory. 182-194
Formal Verification of Programming Language Foundations
- Guillaume Allais, James Chapman, Conor McBride, James McKinna:
Type-and-scope safe programs and their proofs. 195-207 - Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer:
Formally verified differential dynamic logic. 208-221 - Jonas Kaiser, Tobias Tebbi, Gert Smolka:
Equivalence of system f and ź2 in Coq based on context morphism lemmas. 222-234
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-13 20:20 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:
