Proof-assistant-based verification of programs

Proof assistants are now widely used in the field of pro-gramming languages research to reason formally about ob-jects of increasing complexity, like advanced type systems, large programming languages, compilers, or mathematical constructs. This research examination report focuses on the use of proof assistants in reasoning about programs, and surveys the methods developed to tame the complexity of representing languages and their semantics, as well as the difficulties encountered in reasoning about programs in im-perative and concurrent settings. We also examine concrete tools developed to perform this reasoning, and consider their trade-offs in expressivity and proof automation. 1