Theorem proving in higher order logics

More about the book

This collection explores the utility of formal methods in software development and certification, highlighting various techniques and applications. It covers topics such as formal techniques in software engineering, ensuring correct software and safe systems, and the use of separation logic in small-step cminor. The annotation discusses formalizing Java’s data race-free guarantee, finding lexicographic orders for termination proofs in Isabelle/HOL, and extracting purely functional contents from logical inductive types. It also addresses modular formalization of finite group theory and verifying nonlinear real formulas via sums of squares. Expectation properties for discrete random variables in HOL are examined, along with a formally verified prover for description logic. The work includes proof pearls on termination analysis, usability improvements in HOL through automation tactics, and verified decision procedures for context-free grammars. The application of XCAP for certifying realistic systems code is highlighted, alongside discussions on source-level proof reconstruction for interactive theorem proving. The power of higher-order encodings in logical frameworks is emphasized, as well as operational reasoning for concurrent Caml programs. The collection also presents a monad-based modeling and verification toolbox for security protocols, primality proving with elliptic curves, and systems of classical higher-order logic wi