Elamur Research⌕
☰
home / venues / CPP / 2018

CPP 2018 — accepted papers

CPP 2018 is the 2018 edition of the ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). OpenAlex lists 24 papers of it; our library holds 1 with our summaries. Below: the most cited papers, every accepted paper, and ours with their topics, authors and institutions.

 24papers in the proceedings 1work in our library 74citations of these works

Most cited papers

By their OpenAlex citations; a paper with our summary links to its page here, the others to the original.

  1. Towards verifying ethereum smart contract bytecode in Isabelle/HOL ↗Sidney Amani, Myriam Bégel, Maksym Bortin et al.232 citations
  2. Mechanising and verifying the WebAssembly specificationConrad Watt66 citations · our summary
  3. Mechanising blockchain consensus ↗George Pîrlea, Ilya Sergey45 citations
  4. Œuf: minimizing the Coq extraction TCB ↗Eric Mullen, Stuart Pernsteiner, James R. Wilcox et al.37 citations
  5. Total Haskell is reasonable Coq ↗Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah et al.31 citations
  6. A monadic framework for relational verification: applied to information security, program equivalence, and optimizations ↗Niklas Grimm, Kenji Maillard, Cédric Fournet A et al.22 citations
  7. Adapting proof automation to adapt proofs ↗Talia Ringer, Nathaniel Yazdani, John Leo et al.20 citations
  8. A verified SAT solver with watched literals using imperative HOL ↗Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich18 citations
  9. A Coq formalization of normalization by evaluation for Martin-Löf type theory ↗Paweł Wieczorek, Dariusz Biernacki17 citations
  10. A formal proof in Coq of a control function for the inverted pendulum ↗Damien Rouhling17 citations

All accepted papers (24)

The most cited first; 1 with our summary link to their page here, the others to the original.

  1. Towards verifying ethereum smart contract bytecode in Isabelle/HOL ↗Sidney Amani, Myriam Bégel, Maksym Bortin et al.232 citations
  2. Mechanising and verifying the WebAssembly specificationConrad Watt66 citations · our summary
  3. Mechanising blockchain consensus ↗George Pîrlea, Ilya Sergey45 citations
  4. Œuf: minimizing the Coq extraction TCB ↗Eric Mullen, Stuart Pernsteiner, James R. Wilcox et al.37 citations
  5. Total Haskell is reasonable Coq ↗Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah et al.31 citations
  6. A monadic framework for relational verification: applied to information security, program equivalence, and optimizations ↗Niklas Grimm, Kenji Maillard, Cédric Fournet A et al.22 citations
  7. Adapting proof automation to adapt proofs ↗Talia Ringer, Nathaniel Yazdani, John Leo et al.20 citations
  8. A verified SAT solver with watched literals using imperative HOL ↗Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich18 citations
  9. A Coq formalization of normalization by evaluation for Martin-Löf type theory ↗Paweł Wieczorek, Dariusz Biernacki17 citations
  10. A formal proof in Coq of a control function for the inverted pendulum ↗Damien Rouhling17 citations
  11. Finite sets in homotopy type theory ↗Dan Frumin, Herman Geuvers, Léon Gondelman et al.15 citations
  12. Generic derivation of induction for impredicative encodings in Cedille ↗Denis Firsov, Aaron Stump11 citations
  13. Binder aware recursion over well-scoped de Bruijn syntax ↗Jonas Kaiser, Steven Schäfer, Kathrin Stark10 citations
  14. Proofs in conflict-driven theory combination ↗Maria Paola Bonacina, Stéphane Lengrand, Natarajan Shankar8 citations
  15. Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper) ↗Jose Divasón, Sebastiaan J. C. Joosten, Ondřej Kunčar et al.7 citations
  16. Formal microeconomic foundations and the first welfare theorem ↗Cezary Kaliszyk, Julian Parsert7 citations
  17. Large model constructions for second-order ZF in dependent type theory ↗Dominik Kirst, Gert Smolka6 citations
  18. Triangulating context lemmas ↗Craig A. McLaughlin, James McKinna, Ian Stark6 citations
  19. Completeness and decidability of converse PDL in the constructive type theory of Coq ↗Christian Doczkal, Joachim Bard4 citations
  20. HOπ in Coq ↗Sergueï Lenglet, Alan Schmitt3 citations
  21. A constructive formalisation of Semi-algebraic sets and functions ↗Boris Djalal2 citations
  22. Formal proof of polynomial-time complexity with quasi-interpretations ↗Hugo Férée, Samuel Hym, Micaela Mayero et al.2 citations
  23. A two-level logic perspective on (simultaneous) substitutions ↗Kaustuv Chaudhuri1 citation
  24. POPLMark reloaded: mechanizing logical relations proofs (invited talk) ↗Brigitte Pientka1 citation

 Papers with our summary in our library (1)

The most cited first (OpenAlex citations plus our library's).

  1. Mechanising and Verifying the WebAssembly SpecificationACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)Conrad Watt2018 · 74 citations

 Fields

Computer Science (1)

 Top institutions

Institutions on the bylines of its works here, by the number of works.

🎓University of CambridgeCambridge · United Kingdom1 work here

works and citations from OpenAlex and our library.

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2018/