Formal Reasoning About Programs

This is an in-progress, open-source book by Adam Chlipala simultaneously introducing the Coq proof assistant and techniques for proving correctness of programs. That is, the game is doing completely rigorous, machine-checked mathematical proofs, showing that programs meet their specifications.

Just run make here to build everything, including the book frap.pdf and the accompanying Coq source modules.

Code associated with the different chapters

Chapter 2: BasicSyntax.v
Chapter 3: Interpreters.v
Chapter 4: TransitionSystems.v
Chapter 5: ModelChecking.v
Chapter 6: OperationalSemantics.v
Chapter 7: AbstractInterpretation.v
Chapter 8: LambdaCalculusAndTypeSoundness.v
Chapter 9: TypesAndMutation.v
Chapter 10: HoareLogic.v
Chapter 11: DeepAndShallowEmbeddings.v
Chapter 12: SeparationLogic.v
Chapter 13: SharedMemory.v

968 B Raw Blame History

Formal Reasoning About Programs

Code associated with the different chapters

968 B

Raw Blame History