default search action

combined dblp search
author search
venue search
publication search

ask others

7. CPP 2018: Los Angeles, CA, USA

> 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
  - electronic edition @ acm.org
  - details & citations
- export record
  dblp key:
  - conf/cpp/2018
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2018
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

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Pientka18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Pientka18
Brigitte Pientka:
POPLMark reloaded: mechanizing logical relations proofs (invited talk). 1
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DivasonJKT018
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DivasonJKT018
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

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Spector-Zabusky18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Spector-Zabusky18
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich:
Total Haskell is reasonable Coq. 14-27
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Rouhling18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Rouhling18
Damien Rouhling:
A formal proof in Coq of a control function for the inverted pendulum. 28-41
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DoczkalB18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DoczkalB18
Christian Doczkal, Joachim Bard:
Completeness and decidability of converse PDL in the constructive type theory of Coq. 42-52

Verified Applications

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Watt18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Watt18
Conrad Watt:
Mechanising and verifying the WebAssembly specification. 53-65
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AmaniBBS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AmaniBBS18
Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples:
Towards verifying ethereum smart contract bytecode in Isabelle/HOL. 66-77
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/PirleaS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/PirleaS18
George Pîrlea, Ilya Sergey:
Mechanising blockchain consensus. 78-90
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KaliszykP18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KaliszykP18
Cezary Kaliszyk, Julian Parsert:
Formal microeconomic foundations and the first welfare theorem. 91-101

Proof Methods and Libraries

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/McLaughlinMS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/McLaughlinMS18
Craig McLaughlin, James McKinna, Ian Stark:
Triangulating context lemmas. 102-114
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/RingerYLG18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/RingerYLG18
Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman:
Adapting proof automation to adapt proofs. 115-129
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/GrimmMFHMPRRSB18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/GrimmMFHMPRRSB18
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
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FereeHMMN18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FereeHMMN18
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

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FleuryBL18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FleuryBL18
Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich:
A verified SAT solver with watched literals using imperative HOL. 158-171
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/MullenPWTG18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/MullenPWTG18
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman:
Œuf: minimizing the Coq extraction TCB. 172-185
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BonacinaGS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BonacinaGS18
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Proofs in conflict-driven theory combination. 186-200

Type Theory, Set Theory, and Formalized Mathematics

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FruminGGW18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FruminGGW18
Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide:
Finite sets in homotopy type theory. 201-214
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FirsovS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FirsovS18
Denis Firsov, Aaron Stump:
Generic derivation of induction for impredicative encodings in Cedille. 215-227
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KirstS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KirstS18
Dominik Kirst, Gert Smolka:
Large model constructions for second-order ZF in dependent type theory. 228-239
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Djalal18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Djalal18
Boris Djalal:
A constructive formalisation of Semi-algebraic sets and functions. 240-251

Formalizing Meta-Theory

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LengletS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LengletS18
Sergueï Lenglet, Alan Schmitt:
HOπ in Coq. 252-265
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/WieczorekB18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/WieczorekB18
Pawel Wieczorek, Dariusz Biernacki:
A Coq formalization of normalization by evaluation for Martin-Löf type theory. 266-279
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Chaudhuri18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Chaudhuri18
Kaustuv Chaudhuri:
A two-level logic perspective on (simultaneous) substitutions. 280-292
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KaiserSS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KaiserSS18
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.