pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-30 16:16:19 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Formal Reasoning About Programs
248 commits 1 branch 0 tags 1.6 MiB
Coq 80.7%
TeX 19%
OCaml 0.1%
HTML 0.1%
Find a file
Adam Chlipala 0e74bcf948 Push the last code change through a further copy-and-paste instance
2017-02-09 06:58:38 -05:00
.gitignore DeepAndShallowEmbeddings: adding failure 2016-04-10 15:38:47 -04:00
_CoqProject MessagesAndRefinement: comments 2016-05-08 16:58:41 -04: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
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
README.md MessagesAndRefinement: add to README 2016-05-08 19:00:15 -04: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

README.md

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