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. Alternatively, run `make lib' to build just the book library, not the chapter example files or PDF.

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
Chapter 14: ConcurrentSeparationLogic.v
Chapter 15: MessagesAndRefinement.v

1.1 KiB Raw Blame History

Formal Reasoning About Programs

Code associated with the different chapters

1.1 KiB

Raw Blame History