CPP 2016: THE FIFTH INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS

This page contains an index consisting of author-provided keywords.

A
access control	A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Algebra	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
algebraic numbers	Formalization of a Newton series representation of polynomials
automated theorem proving	The Vampire and the FOOL
automation	Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
B
Bisimulation	Bisimulation Up-to Techniques for Psi-calculi
Bisimulation up-to	Bisimulation Up-to Techniques for Psi-calculi
bracket abstraction	Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
C
C	A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
C semantics	Formal Verification of Control-flow Graph Flattening
Calculus	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
compiler correctness	Axiomatic Semantics for Compiler Verification
Complexity	Formalizing Jordan Normal Forms in Isabelle/HOL
Continuity	A Nominal Exploration of Intuitionism
Coq	A Nominal Exploration of Intuitionism Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials A Unified Coq Framework for Verifying C Programs with Floating-Point Computations A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Coquelicot	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Cyber-Physical Systems	A Logic of Proofs for Differential Dynamic Logic
D
Data Structures	Refinement Based Verification of Imperative Data Structures
Decision procedure	A Modular, Efficient Formalisation of Real Algebraic Numbers
Distributed Systems	Planning for Change in a Formal Verification of the Raft Consensus Protocol
Dynamic Logic	A Logic of Proofs for Differential Dynamic Logic
E
e	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Exceptions	A Nominal Exploration of Intuitionism
F
first-order logic	The Vampire and the FOOL
Floating-point computations	A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
formal verification	Axiomatic Semantics for Compiler Verification Planning for Change in a Formal Verification of the Raft Consensus Protocol A Unified Coq Framework for Verifying C Programs with Floating-Point Computations A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
formalization of mathematics	Formalization of a Newton series representation of polynomials
fractions	Formalization of a Newton series representation of polynomials
H
hammers	Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
Higher Inductive Types	Constructing the Propositional Truncation using Non-recursive HITs
Homotopy Type Theory	Constructing the Propositional Truncation using Non-recursive HITs
Hybrid Systems	A Logic of Proofs for Differential Dynamic Logic
I
Imperative	Refinement Based Verification of Imperative Data Structures
Intuitionistic Type Theory	A Nominal Exploration of Intuitionism
Isabelle	Mizar Environment for Isabelle Bisimulation Up-to Techniques for Psi-calculi
Isabelle/HOL	Refinement Based Verification of Imperative Data Structures A Modular, Efficient Formalisation of Real Algebraic Numbers Formalizing Jordan Normal Forms in Isabelle/HOL
Isar	Mizar Environment for Isabelle
J
Jordan normal form	Formalizing Jordan Normal Forms in Isabelle/HOL
L
Lean	Constructing the Propositional Truncation using Non-recursive HITs
Logic of Proofs	A Logic of Proofs for Differential Dynamic Logic
M
Mathematical Components	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Matrix theory	Formalizing Jordan Normal Forms in Isabelle/HOL
Mizar	Mizar Environment for Isabelle
multivariate polynomials	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
N
Newton power series	Formalization of a Newton series representation of polynomials
Nominal Isabelle	Bisimulation Up-to Techniques for Psi-calculi
Nominal Logic	Bisimulation Up-to Techniques for Psi-calculi
Nominal Type Theory	A Nominal Exploration of Intuitionism
Nuprl	A Nominal Exploration of Intuitionism
O
object logic	Mizar Environment for Isabelle
P
pi	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
policy analysis	A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
Polymorphism	Higher-order Representation Predicates in Separation Logic
polynomials	Formalization of a Newton series representation of polynomials
Process calculus	Bisimulation Up-to Techniques for Psi-calculi
program analysis	The Vampire and the FOOL
program correctness	A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
program obfuscation	Formal Verification of Control-flow Graph Flattening
program verification	The Vampire and the FOOL
proof assistants	Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
Proof Engineering	Planning for Change in a Formal Verification of the Raft Consensus Protocol
Proof of transcendence	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
Propositional Truncation	Constructing the Propositional Truncation using Non-recursive HITs
Psi-calculi	Bisimulation Up-to Techniques for Psi-calculi
R
Real algebraic geometry	A Modular, Efficient Formalisation of Real Algebraic Numbers
Recursive ownership	Higher-order Representation Predicates in Separation Logic
Refinement	Refinement Based Verification of Imperative Data Structures
Representation predicates	Higher-order Representation Predicates in Separation Logic
S
Separation Logic	Higher-order Representation Predicates in Separation Logic
Squashing	A Nominal Exploration of Intuitionism
symmetric polynomials	Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
T
Theorem Proving	A Logic of Proofs for Differential Dynamic Logic
TPTP	The Vampire and the FOOL
Truncation	A Nominal Exploration of Intuitionism
V
Vampire	The Vampire and the FOOL
Verification	Refinement Based Verification of Imperative Data Structures
verified compiler	Formal Verification of Control-flow Graph Flattening
W
weakest preconditions	Axiomatic Semantics for Compiler Verification
X
XACML	A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules

Disclaimer | Powered by EasyChair Smart Program