📰 CPP 2019 — accepted papers

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

Most cited papers

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

1. From C to interaction trees: specifying, verifying, and testing a networked server ↗Nicolas C. H. Koh, Yao Li, Yishuai Li et al.47 citations
2. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions ↗Kathrin Stark, Steven Schäfer, Jonas Kaiser39 citations
3. Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk) ↗Jasmin Christian Blanchette32 citations
4. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem ↗Yannick Forster, Dominik Kirst, Gert Smolka25 citations
5. A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra ↗Véronique Benzaken, Évelyne Contejean22 citations
6. Eliminating reflection from type theory ↗Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau22 citations
7. A verified prover based on ordered resolution ↗Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel21 citations
8. Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines ↗Yannick Forster, Dominique Larchey-Wendling17 citations
9. A verified protocol buffer compiler ↗Qianchuan Ye, Benjamin Delaware12 citations
10. Call-by-push-value in Coq: operational, equational, and denotational theory ↗Yannick Forster, Steven Schäfer, Simon Spies et al.11 citations

All accepted papers (21)

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

1. From C to interaction trees: specifying, verifying, and testing a networked server ↗Nicolas C. H. Koh, Yao Li, Yishuai Li et al.47 citations
2. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions ↗Kathrin Stark, Steven Schäfer, Jonas Kaiser39 citations
3. Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk) ↗Jasmin Christian Blanchette32 citations
4. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem ↗Yannick Forster, Dominik Kirst, Gert Smolka25 citations
5. A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra ↗Véronique Benzaken, Évelyne Contejean22 citations
6. Eliminating reflection from type theory ↗Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau22 citations
7. A verified prover based on ordered resolution ↗Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel21 citations
8. Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines ↗Yannick Forster, Dominique Larchey-Wendling17 citations
9. A verified protocol buffer compiler ↗Qianchuan Ye, Benjamin Delaware12 citations
10. Call-by-push-value in Coq: operational, equational, and denotational theory ↗Yannick Forster, Steven Schäfer, Simon Spies et al.11 citations
11. Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions ↗Sandrine Blazy, Rémi Hutin11 citations
12. Formally verified big step semantics out of x86-64 binaries ↗Ian Roessle, Freek Verbeek, Binoy Ravindran11 citations
13. A formal proof of Hensel's lemma over the p-adic integers ↗Robert Y. Lewis8 citations
14. Smooth manifolds and types to sets for linear algebra in Isabelle/HOL ↗Fabian Immler, Bohua Zhan6 citations
15. A proof-theoretic approach to certifying skolemization ↗Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller4 citations
16. A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL ↗Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh et al.4 citations
17. Verified solving and asymptotics of linear recurrences ↗Manuel Eberl4 citations
18. Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem ↗Wenda Li, Lawrence Charles Paulson2 citations
19. Dynamic class initialization semantics: a Jinja extension ↗Susannah Mansky, Elsa L. Gunter1 citation
20. A linear logical framework in Hybrid (invited talk) ↗Amy Felty
21. Certified ACKBO ↗Alexander Lochmann, Christian Sternagel

📄 Papers with our summary in our library (3)

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

1. The Lean mathematical libraryACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)The mathlib Community2019 · 249 citations
2. Exploration of Neural Machine Translation in Autoformalization of Mathematics in MizarACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)Qingxiang Wang, Chad Brown, Cezary Kaliszyk, et al.2019 · 50 citations
3. Formalising perfectoid spacesACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)Kevin Buzzard, Johan Commelin, Patrick Massot2019 · 48 citations

🧭 Top topics

Topics of its works in our library, with the number of works on each.

🧮Reasoning (3)🔁Machine translation (1)

📚 Fields

🖥️Computer Science (3)🎭Arts and Humanities (1)➗Mathematics (1)

🧑‍🔬 Top authors

Authors with a page who published here most often: their works here, and the citations of those works.

🏛️ Top institutions

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

🎓Université Paris-SudOrsay · France1 work here🔬Centre National de la Recherche ScientifiqueParis · France1 work here🎓University of FreiburgFreiburg im Breisgau · Germany1 work here🎓Universität InnsbruckInnsbruck · Austria1 work here🎓Czech Technical University in PraguePrague · Czechia1 work here🎓University of WarsawWarsaw · Poland1 work here🎓Imperial College LondonLondon · 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/2019/