Formal Reasoning About Programs
Find a file
2017-02-16 21:01:23 -05:00
.gitignore DeepAndShallowEmbeddings: adding failure 2016-04-10 15:38:47 -04:00
_CoqProject Start of DataAbstraction: queue examples 2017-02-12 15:19:48 -05:00
AbstractInterpret.v Add AbstractInterpret; fix 8.4 compatibility 2016-03-07 18:49:16 -05:00
AbstractInterpretation.v Address typo reports and other suggestions from Eric Tanter 2016-12-31 13:53:50 -05:00
BasicSyntax.v Push the last code change through a further copy-and-paste instance 2017-02-09 06:58:38 -05:00
BasicSyntax_template.v Small typo fix in BasicSyntax 2017-02-07 15:11:54 -05:00
ConcurrentSeparationLogic.v Fixes for Coq 8.4 2016-05-01 20:09:39 -04:00
ConcurrentSeparationLogic_template.v Fixes for Coq 8.4 2016-05-01 20:09:39 -04:00
DataAbstraction.v DataAbstraction: range sets 2017-02-12 17:49:30 -05:00
DeepAndShallowEmbeddings.v DeepAndShallowEmbeddings: Coq 8.4 support 2016-04-11 08:13:49 -04:00
DeepAndShallowEmbeddings_template.v DeepAndShallowEmbedding_template 2016-04-11 08:30:17 -04:00
DeeperInterp.ml DeepAndShallowEmbeddings: Deep 2016-04-10 15:10:56 -04:00
DeeperWithFailInterp.ml DeepAndShallowEmbeddings: adding failure 2016-04-10 15:38:47 -04:00
DeepInterp.ml DeepAndShallowEmbeddings: Deep 2016-04-10 15:10:56 -04:00
Frap.v Finish port to Coq 8.6 2017-02-07 20:51:13 -05:00
frap_book.tex Typo fixes in Chapter 2 2017-02-07 14:49:38 -05:00
HoareLogic.v HoareLogic: comments 2016-03-27 18:44:35 -04:00
Imp.v Add Imp, recapping OperationalSemantics object language and semantics 2016-03-04 12:49:08 -05:00
index.html Update book index page for this semester 2017-02-08 08:47:18 -05:00
Interpreters.v Rename [map] to [fmap] 2016-02-09 09:07:37 -05:00
Interpreters_template.v For Coq 8.5 compatibility, use [Admitted] instead of [admit] 2016-02-09 18:10:58 -05:00
Invariant.v Add [parallel] to libary 2016-02-22 17:28:40 -05:00
LambdaCalculusAndTypeSoundness.v Fix for Coq 8.5 again 2017-02-07 21:35:23 -05:00
LambdaCalculusAndTypeSoundness_template.v LambdaCalculusAndTypeSoundness_template 2016-03-14 13:14:41 -04:00
Makefile Add SepCancel to 'lib' target 2016-04-19 14:29:02 -04:00
Map.v SeparationLogic: soundness proof 2016-04-17 16:55:52 -04:00
MessagesAndRefinement.v MessagesAndRefinement: Coq 8.4 compatibility 2016-05-09 10:42:13 -04:00
ModelCheck.v SharedMemory: model-checking example, after tweaking library 2016-04-21 13:42:30 -04:00
ModelChecking.v Tweaked Ltac singletoner to display state space exploration in real time 2016-02-22 17:53:31 -05:00
ModelChecking_template.v ModelChecking_template 2016-02-22 09:45:53 -05:00
OperationalSemantics.v Add Imp, recapping OperationalSemantics object language and semantics 2016-03-04 12:49:08 -05:00
OperationalSemantics_template.v Progress on porting to Coq 8.6 2017-02-07 18:51:05 -05:00
Polymorphism.v Polymorphism: add a comment about the infamous quantifier-ordering issue with induction 2017-02-15 10:01:49 -05:00
Polymorphism_template.v Polymorphism template 2017-02-09 13:51:16 -05:00
README.md Correct filename in README 2017-02-09 13:54:58 -05:00
Relations.v SharedMemory: first optimization 2016-04-21 19:12:02 -04:00
SeparationLogic.v Progress on porting to Coq 8.6 2017-02-07 18:51:05 -05:00
SeparationLogic_template.v Progress on porting to Coq 8.6 2017-02-07 18:51:05 -05:00
SepCancel.v Finalizing ConcurrentSeparationLogic 2016-05-01 19:45:51 -04:00
Sets.v Sets: change parsing precedence 2016-04-26 13:46:48 -04:00
SharedMemory.v Finish port to Coq 8.6 2017-02-07 20:51:13 -05:00
TransitionSystems.v Harmonize inductive-definition convention 2016-02-16 11:41:30 -05:00
TransitionSystems_template.v Harmonize inductive-definition convention 2016-02-16 11:41:30 -05:00
TypesAndMutation.v Fix for Coq 8.5 again 2017-02-07 21:35:23 -05:00
Var.v Interpreters: factorial example 2016-02-06 22:09:37 -05:00

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_book.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

The main narrative, also present in the book PDF, presents standard program-proof ideas, without rigorous proofs. Matching Coq files here show how to make it rigorous. Interleaved with that narrative, there are also other lectures' worth of material, for building up more practical background on Coq itself. That secondary track appears in this list, too, at a higher level of indentation.

  • Chapter 2: BasicSyntax.v
    • Polymorphism.v: polymorphism and generic data structures
  • 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