CPP 2019
21 papers
- A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra
- A formal proof of hensel's lemma over the p-adic integers
- A linear logical framework in hybrid (invited talk)
- A proof-theoretic approach to certifying skolemization
- A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL
- A verified protocol buffer compiler
- A verified prover based on ordered resolution
- Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions
- Call-by-push-value in coq: operational, equational, and denotational theory
- Certified ACKBO
- Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines
- Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem
- Dynamic class initialization semantics: a jinja extension
- Eliminating reflection from type theory
- Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions
- Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)
- Formally verified big step semantics out of x86-64 binaries
- From C to interaction trees: specifying, verifying, and testing a networked server
- On synthetic undecidability in coq, with an application to the entscheidungsproblem
- Smooth manifolds and types to sets for linear algebra in Isabelle/HOL
- Verified solving and asymptotics of linear recurrences