---
title: "CPP 2019 — accepted papers — Elamur Research"
description: "CPP 2019 — accepted papers: 3 papers 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/2019/"
---
[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/2019/)

[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/) / 2019

# 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.

[**21** papers in the proceedings](#all) · [**3** works in our library](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2019/#works) · [**347** citations of these works](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2019/#works)

## 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 ↗](https://doi.org/10.1145/3293880.3294106)**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 ↗](https://doi.org/10.1145/3293880.3294101)**Kathrin Stark, Steven Schäfer, Jonas Kaiser*39 citations*
3. **[Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk) ↗](https://doi.org/10.1145/3293880.3294087)**Jasmin Christian Blanchette*32 citations*
4. **[On synthetic undecidability in Coq, with an application to the Entscheidungsproblem ↗](https://doi.org/10.1145/3293880.3294091)**Yannick Forster, Dominik Kirst, Gert Smolka*25 citations*
5. **[A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra ↗](https://doi.org/10.1145/3293880.3294107)**Véronique Benzaken, Évelyne Contejean*22 citations*
6. **[Eliminating reflection from type theory ↗](https://doi.org/10.1145/3293880.3294095)**Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau*22 citations*
7. **[A verified prover based on ordered resolution ↗](https://doi.org/10.1145/3293880.3294100)**Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel*21 citations*
8. **[Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines ↗](https://doi.org/10.1145/3293880.3294096)**Yannick Forster, Dominique Larchey-Wendling*17 citations*
9. **[A verified protocol buffer compiler ↗](https://doi.org/10.1145/3293880.3294105)**Qianchuan Ye, Benjamin Delaware*12 citations*
10. **[Call-by-push-value in Coq: operational, equational, and denotational theory ↗](https://doi.org/10.1145/3293880.3294097)**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 ↗](https://doi.org/10.1145/3293880.3294106)**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 ↗](https://doi.org/10.1145/3293880.3294101)**Kathrin Stark, Steven Schäfer, Jonas Kaiser*39 citations*
3. **[Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk) ↗](https://doi.org/10.1145/3293880.3294087)**Jasmin Christian Blanchette*32 citations*
4. **[On synthetic undecidability in Coq, with an application to the Entscheidungsproblem ↗](https://doi.org/10.1145/3293880.3294091)**Yannick Forster, Dominik Kirst, Gert Smolka*25 citations*
5. **[A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra ↗](https://doi.org/10.1145/3293880.3294107)**Véronique Benzaken, Évelyne Contejean*22 citations*
6. **[Eliminating reflection from type theory ↗](https://doi.org/10.1145/3293880.3294095)**Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau*22 citations*
7. **[A verified prover based on ordered resolution ↗](https://doi.org/10.1145/3293880.3294100)**Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel*21 citations*
8. **[Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines ↗](https://doi.org/10.1145/3293880.3294096)**Yannick Forster, Dominique Larchey-Wendling*17 citations*
9. **[A verified protocol buffer compiler ↗](https://doi.org/10.1145/3293880.3294105)**Qianchuan Ye, Benjamin Delaware*12 citations*
10. **[Call-by-push-value in Coq: operational, equational, and denotational theory ↗](https://doi.org/10.1145/3293880.3294097)**Yannick Forster, Steven Schäfer, Simon Spies et al.*11 citations*
11. **[Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions ↗](https://doi.org/10.1145/3293880.3294103)**Sandrine Blazy, Rémi Hutin*11 citations*
12. **[Formally verified big step semantics out of x86-64 binaries ↗](https://doi.org/10.1145/3293880.3294102)**Ian Roessle, Freek Verbeek, Binoy Ravindran*11 citations*
13. **[A formal proof of Hensel's lemma over the p-adic integers ↗](https://doi.org/10.1145/3293880.3294089)**Robert Y. Lewis*8 citations*
14. **[Smooth manifolds and types to sets for linear algebra in Isabelle/HOL ↗](https://doi.org/10.1145/3293880.3294093)**Fabian Immler, Bohua Zhan*6 citations*
15. **[A proof-theoretic approach to certifying skolemization ↗](https://doi.org/10.1145/3293880.3294094)**Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller*4 citations*
16. **[A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL ↗](https://doi.org/10.1145/3293880.3294098)**Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh et al.*4 citations*
17. **[Verified solving and asymptotics of linear recurrences ↗](https://doi.org/10.1145/3293880.3294090)**Manuel Eberl*4 citations*
18. **[Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem ↗](https://doi.org/10.1145/3293880.3294092)**Wenda Li, Lawrence Charles Paulson*2 citations*
19. **[Dynamic class initialization semantics: a Jinja extension ↗](https://doi.org/10.1145/3293880.3294104)**Susannah Mansky, Elsa L. Gunter*1 citation*
20. **[A linear logical framework in Hybrid (invited talk) ↗](https://doi.org/10.1145/3293880.3294088)**Amy Felty
21. **[Certified ACKBO ↗](https://doi.org/10.1145/3293880.3294099)**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 library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/) [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/)**The mathlib Community*2019 · 249 citations*
2. **[Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/) [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/)**Qingxiang Wang, Chad Brown, Cezary Kaliszyk, et al.*2019 · 50 citations*
3. **[Formalising perfectoid spaces](https://md.research.elamur.ai/free/en/papers/buzzard-2019-formalising-perfectoid-spaces/) [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/)**Kevin Buzzard, Johan Commelin, Patrick Massot*2019 · 48 citations*

## Top topics

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

[Reasoning (3)](https://md.research.elamur.ai/free/en/topics/reasoning/) · [Machine translation (1)](https://md.research.elamur.ai/free/en/topics/machine-translation/)

## Fields

[Computer Science (3)](https://md.research.elamur.ai/free/en/shelves/computer-science/) · [Arts and Humanities (1)](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · [Mathematics (1)](https://md.research.elamur.ai/free/en/shelves/mathematics/)

## Top authors

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

[🧑‍🔬**Cezary Kaliszyk**1 work here · 50 citations](https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/) · [🧑‍🔬**Josef Urban**1 work here · 50 citations](https://md.research.elamur.ai/free/en/authors/josef-urban/) · [🧑‍🔬**Qingxiang Wang**1 work here · 50 citations](https://md.research.elamur.ai/free/en/authors/qingxiang-wang/)

## Top institutions

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

[🎓**Université Paris-Sud** Orsay · France 1 work here](https://md.research.elamur.ai/free/en/universities/universite-paris-sud/) · [🔬**Centre National de la Recherche Scientifique** Paris · France 1 work here](https://md.research.elamur.ai/free/en/labs/centre-national-de-la-recherche-scientifique/) · [🎓**University of Freiburg** Freiburg im Breisgau · Germany 1 work here](https://md.research.elamur.ai/free/en/universities/university-of-freiburg/) · [🎓**Universität Innsbruck** Innsbruck · Austria 1 work here](https://md.research.elamur.ai/free/en/universities/universitat-innsbruck/) · [🎓**Czech Technical University in Prague** Prague · Czechia 1 work here](https://md.research.elamur.ai/free/en/universities/czech-technical-university-in-prague/) · [🎓**University of Warsaw** Warsaw · Poland 1 work here](https://md.research.elamur.ai/free/en/universities/university-of-warsaw/) · [🎓**Imperial College London** London · United Kingdom 1 work here](https://md.research.elamur.ai/free/en/universities/imperial-college-london/)

works and citations from OpenAlex and our library.

- [← previous CPP 2018](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2018/)
- [↑ back to CPP](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/)