default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID8th CPP 2019: Cascais, Portugal
- 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
- Jasmin Christian Blanchette
:
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). 1-13 - Amy P. Felty:
A linear logical framework in hybrid (invited talk). 14
Formalization of Mathematics and Computer Algebra
- Robert Y. Lewis:
A formal proof of hensel's lemma over the p-adic integers. 15-26 - Manuel Eberl:
Verified solving and asymptotics of linear recurrences. 27-37 - Yannick Forster, Dominik Kirst, Gert Smolka:
On synthetic undecidability in coq, with an application to the entscheidungsproblem. 38-51 - Wenda Li, Lawrence C. Paulson:
Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. 52-64 - Fabian Immler, Bohua Zhan:
Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. 65-77
Proof Theory, Theory of Programming Languages
- Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller:
A proof-theoretic approach to certifying skolemization. 78-90 - Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau:
Eliminating reflection from type theory. 91-103 - Yannick Forster, Dominique Larchey-Wendling:
Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. 104-117 - 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
- 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 - Alexander Lochmann, Christian Sternagel:
Certified ACKBO. 144-151 - Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel:
A verified prover based on ordered resolution. 152-165 - Kathrin Stark, Steven Schäfer, Jonas Kaiser:
Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. 166-180
Program Verification
- Ian Roessle, Freek Verbeek, Binoy Ravindran:
Formally verified big step semantics out of x86-64 binaries. 181-195 - Sandrine Blazy, Rémi Hutin:
Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. 196-208 - Susannah Mansky, Elsa L. Gunter:
Dynamic class initialization semantics: a jinja extension. 209-221 - Qianchuan Ye, Benjamin Delaware:
A verified protocol buffer compiler. 222-233 - 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 - 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.
last updated on 2025-12-14 23:19 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
