CPP 2016
20 papers
- A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics
- A modular, efficient formalisation of real algebraic numbers
- A nominal exploration of intuitionism
- A unified Coq framework for verifying C programs with floating-point computations
- A verified algorithm for detecting conflicts in XACML access control rules
- Axiomatic semantics for compiler verification
- Bisimulation up-to techniques for psi-calculi
- Constructing the propositional truncation using non-recursive HITs
- Dependent type practice (invited talk)
- Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
- Formal verification of control-flow graph flattening
- Formalization of a newton series representation of polynomials
- Formalizing jordan normal forms in Isabelle/HOL
- Higher-order representation predicates in separation logic
- Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
- Perspectives on formal verification (invited talk)
- Planning for change in a formal verification of the raft consensus protocol
- Refinement based verification of imperative data structures
- The vampire and the FOOL
- Towards a mizar environment for isabelle: foundations and language