Harry R. Schwartz

The first DeepSpec Summer School on verified systems is wrapping up. We’ve spent the last couple of weeks learning to use Coq to verify compilers, operating systems, data structures, and file systems.

We reached the consensus that Coq’s documentation isn’t as approachable as it might be. We’ve begun organizing an effort to improve it.

As part of that, we’re combing through our (extremely active) internal Slack group in preparation for publishing some of the tips and strategies we discussed and developed. I offered to clean up the #recommended-readings channel, where folks recommended papers and other readings that they thought might be of general interest.

Our main textbooks

• Pierce et al.’s Software Foundations was our primary introduction to Coq.
• Adam Chlipala’s Certified Programming with Dependent Types is a more fast-paced introduction, with advanced material on the Ltac tactics language, the Coq module system, etc.

Other recommended papers and resources

• Kennedy et al., Coq: The world’s best macro assembler?, PPDP ‘13.
• Ken Thompson, Reflections on Trusting Trust, CACM ‘84.
• Andrew Appel, Verification of a Cryptographic Primitive: SHA-256, TOPLAS ‘15.
• George and Appel, Iterated Register Coalescing, TOPLAS ‘96.
• Bertot and Castéran, Coq’Art: The Calculus of Inductive Constructions. A useful book, but out of date. An up-to-date online version is maintained, but only in French.
• Wu, Appel, and Stump, Foundational Proof Checkers with Small Witnesses, PPDP ‘03.
• Lee et al., Taming Undefined Behavior in LLVM, PLDI ‘17.
• Jung et al., RustBelt: Securing the Foundations of the Rust Programming Language, POPL ‘18.
• Witzel, Sarovar, and Rudinger, Versatile Formal Methods Applied to Quantum Information, 2015.
• Wilcox et al., Verdi: A Framework for Implementing and Formally Verifying Distributed Systems, PLDI ‘15.
• John Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, LICS ‘02.
• Andrew Appel, Program Logics for Certified Compilers. Another resource for learning separation logic.
• Robin Milner, A Theory of Type Polymorphism in Programming, 1978.
• Steele and Sussman, Lambda: The Ultimate Imperative, 1976.
• Guy Steele, Lambda: The Ultimate Declarative, 1976.
• Amadio and Cardelli, Subtyping Recursive Types, TOPLAS ‘93.
• Adam Chlipala, The Bedrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier, ICFP ‘13.

Some papers specifically related to QuickChick

• Claessen and Hughes, QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, ICFP ‘00. The original QuickCheck paper, which describes some of the typeclass trickery required.
• Paraskevopoulou et al., Foundational Property-Based Testing, ITP ‘15. The original QuickChick paper, focusing on a framework for proving the correctness of generators.
• Hritcu et al., Testing Noninterference, Quickly, ICFP ‘13. A case study on testing information flow control machines.