mirror of
https://github.com/achlipala/frap.git
synced 2024-09-20 04:07:13 +00:00
22 lines
1.1 KiB
Markdown
22 lines
1.1 KiB
Markdown
# Formal Reasoning About Programs
|
|
|
|
This is an in-progress, open-source book by [Adam Chlipala](http://adam.chlipala.net/) simultaneously introducing [the Coq proof assistant](http://coq.inria.fr/) 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`
|