QuickChick: Property-Based Testing for Coq

Language: English Existing skills or strong desire to learn: • functional programming (e.g. OCaml or Haskell), • property-based testing (e.g. QuickCheck), • interactive theorem proving in the Coq proof assistant, • optional: SSReflect, logic programming, constraint programming, probabilistic programming Research Context Designing complex systems that provide strong safety and security guarantees is challenging (e.g. programming languages, language compilers and runtimes, reference monitors, operating systems, hardware, etc). Proof assistants such as Coq (The Coq team, 1984-now) are invaluable for showing formally that such systems indeed satisfy the properties intended by their designers. However, carrying out formal proofs while designing even a relatively simple system can be an exercise in frustration, with a great deal of time spent attempting to prove things about broken definitions, and countless iterations for discovering the correct lemmas and strengthening inductive invariants. The long-term goal of this project1 is to reduce the cost of producing formally verified systems by integratin