--- title: "CPP 2018 — accepted papers — Elamur Research" description: "CPP 2018 — accepted papers: 1 paper in the Elamur Research library, with our summaries, ranked by citations." canonical: "https://research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2018/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2018/) [home](https://md.research.elamur.ai/free/en/) / [venues](https://md.research.elamur.ai/free/en/venues/) / [CPP](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-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. [**24** papers in the proceedings](#all) · [**1** work in our library](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2018/#works) · [**74** citations of these works](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2018/#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 ↗](https://doi.org/10.1145/3167084)**Sidney Amani, Myriam Bégel, Maksym Bortin et al.*232 citations* 2. **[Mechanising and verifying the WebAssembly specification](https://md.research.elamur.ai/free/en/papers/watt-2018-mechanising-verifying-webassembly-specification/)**Conrad Watt*66 citations · our summary* 3. **[Mechanising blockchain consensus ↗](https://doi.org/10.1145/3167086)**George Pîrlea, Ilya Sergey*45 citations* 4. **[Œuf: minimizing the Coq extraction TCB ↗](https://doi.org/10.1145/3167089)**Eric Mullen, Stuart Pernsteiner, James R. Wilcox et al.*37 citations* 5. **[Total Haskell is reasonable Coq ↗](https://doi.org/10.1145/3167092)**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 ↗](https://doi.org/10.1145/3167090)**Niklas Grimm, Kenji Maillard, Cédric Fournet A et al.*22 citations* 7. **[Adapting proof automation to adapt proofs ↗](https://doi.org/10.1145/3167094)**Talia Ringer, Nathaniel Yazdani, John Leo et al.*20 citations* 8. **[A verified SAT solver with watched literals using imperative HOL ↗](https://doi.org/10.1145/3167080)**Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich*18 citations* 9. **[A Coq formalization of normalization by evaluation for Martin-Löf type theory ↗](https://doi.org/10.1145/3167091)**Paweł Wieczorek, Dariusz Biernacki*17 citations* 10. **[A formal proof in Coq of a control function for the inverted pendulum ↗](https://doi.org/10.1145/3167101)**Damien Rouhling*17 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 ↗](https://doi.org/10.1145/3167084)**Sidney Amani, Myriam Bégel, Maksym Bortin et al.*232 citations* 2. **[Mechanising and verifying the WebAssembly specification](https://md.research.elamur.ai/free/en/papers/watt-2018-mechanising-verifying-webassembly-specification/)**Conrad Watt*66 citations · our summary* 3. **[Mechanising blockchain consensus ↗](https://doi.org/10.1145/3167086)**George Pîrlea, Ilya Sergey*45 citations* 4. **[Œuf: minimizing the Coq extraction TCB ↗](https://doi.org/10.1145/3167089)**Eric Mullen, Stuart Pernsteiner, James R. Wilcox et al.*37 citations* 5. **[Total Haskell is reasonable Coq ↗](https://doi.org/10.1145/3167092)**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 ↗](https://doi.org/10.1145/3167090)**Niklas Grimm, Kenji Maillard, Cédric Fournet A et al.*22 citations* 7. **[Adapting proof automation to adapt proofs ↗](https://doi.org/10.1145/3167094)**Talia Ringer, Nathaniel Yazdani, John Leo et al.*20 citations* 8. **[A verified SAT solver with watched literals using imperative HOL ↗](https://doi.org/10.1145/3167080)**Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich*18 citations* 9. **[A Coq formalization of normalization by evaluation for Martin-Löf type theory ↗](https://doi.org/10.1145/3167091)**Paweł Wieczorek, Dariusz Biernacki*17 citations* 10. **[A formal proof in Coq of a control function for the inverted pendulum ↗](https://doi.org/10.1145/3167101)**Damien Rouhling*17 citations* 11. **[Finite sets in homotopy type theory ↗](https://doi.org/10.1145/3167085)**Dan Frumin, Herman Geuvers, Léon Gondelman et al.*15 citations* 12. **[Generic derivation of induction for impredicative encodings in Cedille ↗](https://doi.org/10.1145/3167087)**Denis Firsov, Aaron Stump*11 citations* 13. **[Binder aware recursion over well-scoped de Bruijn syntax ↗](https://doi.org/10.1145/3167098)**Jonas Kaiser, Steven Schäfer, Kathrin Stark*10 citations* 14. **[Proofs in conflict-driven theory combination ↗](https://doi.org/10.1145/3167096)**Maria Paola Bonacina, Stéphane Lengrand, Natarajan Shankar*8 citations* 15. **[Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper) ↗](https://doi.org/10.1145/3167103)**Jose Divasón, Sebastiaan J. C. Joosten, Ondřej Kunčar et al.*7 citations* 16. **[Formal microeconomic foundations and the first welfare theorem ↗](https://doi.org/10.1145/3167100)**Cezary Kaliszyk, Julian Parsert*7 citations* 17. **[Large model constructions for second-order ZF in dependent type theory ↗](https://doi.org/10.1145/3167095)**Dominik Kirst, Gert Smolka*6 citations* 18. **[Triangulating context lemmas ↗](https://doi.org/10.1145/3167081)**Craig A. McLaughlin, James McKinna, Ian Stark*6 citations* 19. **[Completeness and decidability of converse PDL in the constructive type theory of Coq ↗](https://doi.org/10.1145/3167088)**Christian Doczkal, Joachim Bard*4 citations* 20. **[HOπ in Coq ↗](https://doi.org/10.1145/3167083)**Sergueï Lenglet, Alan Schmitt*3 citations* 21. **[A constructive formalisation of Semi-algebraic sets and functions ↗](https://doi.org/10.1145/3167099)**Boris Djalal*2 citations* 22. **[Formal proof of polynomial-time complexity with quasi-interpretations ↗](https://doi.org/10.1145/3167097)**Hugo Férée, Samuel Hym, Micaela Mayero et al.*2 citations* 23. **[A two-level logic perspective on (simultaneous) substitutions ↗](https://doi.org/10.1145/3167093)**Kaustuv Chaudhuri*1 citation* 24. **[POPLMark reloaded: mechanizing logical relations proofs (invited talk) ↗](https://doi.org/10.1145/3167102)**Brigitte Pientka*1 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 Specification](https://md.research.elamur.ai/free/en/papers/watt-2018-mechanising-verifying-webassembly-specification/) [ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/)**Conrad Watt*2018 · 74 citations* ## Fields [Computer Science (1)](https://md.research.elamur.ai/free/en/shelves/computer-science/) ## Top institutions Institutions on the bylines of its works here, by the number of works. [🎓**University of Cambridge** Cambridge · United Kingdom 1 work here](https://md.research.elamur.ai/free/en/universities/university-of-cambridge/) works and citations from OpenAlex and our library. - [next → CPP 2019](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2019/) - [↑ back to CPP](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/)