|
We welcome submissions in research areas related to formal certification of programs and proofs. The following is a non-exhaustive list of topics of interest to CPP:
- certified or certifying programming, compilation, linking, OS kernels, runtime systems, security monitors, and hardware;
- certified mathematical libraries and mathematical theorems;
- proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL4, HOL Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc);
- new languages and tools for certified programming;
- program analysis, program verification, and program synthesis;
- program logics, type systems, and semantics for certified code;
- logics for certifying concurrent and distributed systems;
- mechanized metatheory, formalized programming language semantics, and logical frameworks;
- higher-order logics, dependent type theory, proof theory, logical systems, separation logics, and logics for security;
- verification of correctness and security properties;
- formally verified blockchains and smart contracts;
- certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest;
- certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification;
- certificates for program termination;
- formal models of computation;
- mechanized (un)decidability and computational complexity proofs;
- formally certified methods for induction and coinduction;
- integration of interactive and automated provers;
- logical foundations of proof assistants;
- applications of AI and machine learning to formal certification;
- user interfaces for proof assistants and theorem provers;
- teaching mathematics and computer science with proof assistants. |
