default search action

combined dblp search
author search
venue search
publication search

ask others

6. CPP 2017: Paris, France

> 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/2017
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2017
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

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Paulson17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Paulson17
Lawrence C. Paulson:
Porting the HOL light analysis library: some lessons (invited talk). 1
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Feng17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Feng17
Xinyu Feng:
Mechanized verification of preemptive OS kernels (invited talk). 2

Algorithm and Library Verification

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Pottier17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Pottier17
François Pottier:
Verifying a hash table and its iterators in higher-order separation logic. 3-16
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DivasonJT017
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DivasonJT017
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A formalization of the Berlekamp-Zassenhaus factorization algorithm. 17-29
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AffeldtC17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AffeldtC17
Reynald Affeldt, Cyril Cohen:
Formal foundations of 3D geometry to model robot manipulators. 30-42

Automated Proof and Its Formal Verification

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/JakubuvU17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/JakubuvU17
Jan Jakubuv, Josef Urban:
BliStrTune: hierarchical invention of theorem proving strategies. 43-52
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/RoweB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/RoweB17
Reuben N. S. Rowe, James Brotherston:
Automatic cyclic termination proofs for recursive procedures in separation logic. 53-65
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/YamamotoSM17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/YamamotoSM17
Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto:
Formalization of Karp-Miller tree construction on petri nets. 66-78

Formalized Mathematics with Numerical Computations

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BoldoCFMM17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BoldoCFMM17
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero:
A Coq formal proof of the LaxMilgram theorem. 79-89
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Martin-DorelR17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Martin-DorelR17
Érik Martin-Dorel, Pierre Roux:
A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. 90-99
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Holzl17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Holzl17
Johannes Hölzl:
Markov processes in Isabelle/HOL. 100-111
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Gilbert17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Gilbert17
Gaëtan Gilbert:
Formalising real numbers in homotopy type theory. 112-124

Verified Programming Tools

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FoxMTK17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FoxMTK17
Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar:
Verified compilation of CakeML to multiple machine-code targets. 125-137
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AmaniABLRT17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AmaniABLRT17
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong:
Complx: a verification framework for concurrent imperative programs. 138-150
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ManskyPZD17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ManskyPZD17
William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti:
Verifying dynamic race detection. 151-163

Homotopy Type Theory

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BauerGLSSS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BauerGLSSS17
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
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CockxD17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CockxD17
Jesper Cockx, Dominique Devriese:
Lifting proof-relevant unification to higher dimensions. 173-181
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BoulierPT17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BoulierPT17
Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau:
The next 700 syntactical models of type theory. 182-194

Formal Verification of Programming Language Foundations

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Allais0MM17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Allais0MM17
Guillaume Allais, James Chapman, Conor McBride, James McKinna:
Type-and-scope safe programs and their proofs. 195-207
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BohrerRVVP17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BohrerRVVP17
Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer:
Formally verified differential dynamic logic. 208-221
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KaiserTS17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KaiserTS17
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.