What will it take to build a world in which programmers of all skill levels can formally prove the absence of costly or dangerous bugs in software systems? This seminar will explore technologies for automating formal proofs about software systems in proof assistants like Coq, Lean, or Isabelle/HOL.
Example topics include languages for proof automation, automated theorem proving for proof assistants, plugins and transformations, neural proof synthesis, and usable automation. These topics will be explored through a combination of paper reading and collaborative exploration of code artifacts.
Background in functional programming is expected; background in proof assistants is not needed.