default search action

combined dblp search
author search
venue search
publication search

ask others

8th CPP 2019: Cascais, Portugal

> 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
  - no references & citations available
- export record
  dblp key:
  - conf/cpp/2019
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2019
Assia Mahboubi, Magnus O. Myreen:
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. ACM 2019, ISBN 978-1-4503-6222-1

Invited Talks

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Blanchette19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Blanchette19
Jasmin Christian Blanchette:
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). 1-13
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Felty19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Felty19
Amy P. Felty:
A linear logical framework in hybrid (invited talk). 14

Formalization of Mathematics and Computer Algebra

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Lewis19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Lewis19
Robert Y. Lewis:
A formal proof of hensel's lemma over the p-adic integers. 15-26
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Eberl19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Eberl19
Manuel Eberl:
Verified solving and asymptotics of linear recurrences. 27-37
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/0002KS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/0002KS19
Yannick Forster, Dominik Kirst, Gert Smolka:
On synthetic undecidability in coq, with an application to the entscheidungsproblem. 38-51
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LiP19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LiP19
Wenda Li, Lawrence C. Paulson:
Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. 52-64
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ImmlerZ19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ImmlerZ19
Fabian Immler, Bohua Zhan:
Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. 65-77

Proof Theory, Theory of Programming Languages

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ChaudhuriM019
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ChaudhuriM019
Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller:
A proof-theoretic approach to certifying skolemization. 78-90
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/WinterhalterST19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/WinterhalterST19
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau:
Eliminating reflection from type theory. 91-103
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ForsterL19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ForsterL19
Yannick Forster, Dominique Larchey-Wendling:
Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. 104-117
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ForsterSSS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ForsterSSS19
Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark:
Call-by-push-value in coq: operational, equational, and denotational theory. 118-131

Rewriting, Automated Reasoning

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FelgenhauerMPR19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FelgenhauerMPR19
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp:
A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL. 132-143
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LochmannS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LochmannS19
Alexander Lochmann, Christian Sternagel:
Certified ACKBO. 144-151
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/SchlichtkrullBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/SchlichtkrullBT19
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel:
A verified prover based on ordered resolution. 152-165
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/StarkSK19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/StarkSK19
Kathrin Stark, Steven Schäfer, Jonas Kaiser:
Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. 166-180

Program Verification

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/RoessleVR19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/RoessleVR19
Ian Roessle, Freek Verbeek, Binoy Ravindran:
Formally verified big step semantics out of x86-64 binaries. 181-195
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BlazyH19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BlazyH19
Sandrine Blazy, Rémi Hutin:
Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. 196-208
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ManskyG19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ManskyG19
Susannah Mansky, Elsa L. Gunter:
Dynamic class initialization semantics: a jinja extension. 209-221
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/YeD19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/YeD19
Qianchuan Ye, Benjamin Delaware:
A verified protocol buffer compiler. 222-233
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Koh0LXBHMPZ19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Koh0LXBHMPZ19
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic:
From C to interaction trees: specifying, verifying, and testing a networked server. 234-248
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BenzakenC19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BenzakenC19
Véronique Benzaken, Evelyne Contejean:
A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. 249-261

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.