Formal Reasoning About Programs
Find a file
2017-11-18 11:45:26 -05:00
.gitignore Change ProofByReflection to work in Coq 8.6.1 2017-11-18 10:43:08 -05:00
_CoqProject DependentInductiveTypes 2017-04-02 20:50:10 -04:00
AbstractInterpret.v Bump chapter numbers in Coq code comments 2017-02-21 09:00:30 -05:00
AbstractInterpretation.v Bump chapter numbers in Coq code comments 2017-02-21 09:00:30 -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
CompilerCorrectness.v Working with Coq 8.5pl2 again 2017-11-18 11:45:26 -05:00
CompilerCorrectness_template.v Working with Coq 8.5pl2 again 2017-11-18 11:45:26 -05:00
ConcurrentSeparationLogic.v Start of CompilerCorrectness: cfoldExprs_ok 2017-03-18 14:42:13 -04:00
ConcurrentSeparationLogic_template.v Optimizing tactics for faster state-space exploration 2017-03-05 20:46:53 -05:00
DataAbstraction.v Start of DataAbstraction book chapter 2017-02-20 16:06:33 -05:00
DataAbstraction_template.v DataAbstraction_template 2017-02-21 09:15:33 -05:00
DeepAndShallowEmbeddings.v DeepAndShallowEmbeddings: comment typo fix 2017-04-24 09:28:48 -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
DependentInductiveTypes.v Working with Coq 8.5pl2 again 2017-11-18 11:45:26 -05:00
Frap.v SubsetTypes 2017-03-21 19:27:36 -04:00
frap_book.tex Working with Coq 8.5pl2 again 2017-11-18 11:45:26 -05:00
FrapWithoutSets.v Make [sets] tactic more robust to type synonyms 2017-05-14 12:50:18 -04:00
HoareLogic.v Fix typo 2017-05-05 21:32:14 -04:00
Imp.v Add Imp, recapping OperationalSemantics object language and semantics 2016-03-04 12:49:08 -05:00
index.html Add web links to exercises 2017-06-03 12:54:51 -04:00
Interpreters.v Merge 2017-03-18 20:20:23 -04:00
Interpreters_template.v For Coq 8.5 compatibility, use [Admitted] instead of [admit] 2016-02-09 18:10:58 -05:00
IntroToProofScripting.v IntroToProofScripting_template 2017-03-01 14:14:59 -05:00
IntroToProofScripting_template.v IntroToProofScripting_template 2017-03-01 14:14:59 -05:00
Invariant.v Add [parallel] to libary 2016-02-22 17:28:40 -05:00
LambdaCalculusAndTypeSoundness.v Start of CompilerCorrectness: cfoldExprs_ok 2017-03-18 14:42:13 -04:00
LambdaCalculusAndTypeSoundness_template.v Tiny revisions to LambdaCalculusAndTypeSoundness 2017-04-02 19:18:34 -04:00
LogicProgramming.v Merge branch 'master' of ssh://schizomaniac.net//home/adamc/git-root/frap 2017-03-18 12:30:55 -04:00
LogicProgramming_template.v Fix title in comments 2017-03-15 12:01:28 -04:00
Makefile Add SepCancel to 'lib' target 2016-04-19 14:29:02 -04:00
Map.v SubsetTypes 2017-03-21 19:27:36 -04:00
MessagesAndRefinement.v Typo fix 2017-05-14 15:58:04 -04:00
ModelCheck.v SubsetTypes 2017-03-21 19:27:36 -04:00
ModelChecking.v Optimizing tactics for faster state-space exploration 2017-03-05 20:46:53 -05:00
ModelChecking_sol.v Tweak files for ModelChecking in class 2017-03-06 09:44:29 -05:00
ModelChecking_template.v Tweak files for ModelChecking in class 2017-03-06 09:44:29 -05:00
OperationalSemantics.v Bump chapter numbers in Coq code comments 2017-02-21 09:00:30 -05:00
OperationalSemantics_template.v Tweak OperationalSemantics_template.v 2017-03-13 10:51:40 -04: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
ProofByReflection.v Change ProofByReflection to work in Coq 8.6.1 2017-11-18 10:43:08 -05:00
ProofByReflection_template.v ProofByReflection_template 2017-03-08 14:05:46 -05:00
README.md DependentInductiveTypes 2017-04-02 20:50:10 -04:00
Relations.v SharedMemory: first optimization 2016-04-21 19:12:02 -04:00
SeparationLogic.v Start of CompilerCorrectness: cfoldExprs_ok 2017-03-18 14:42:13 -04: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 SubsetTypes 2017-03-21 19:27:36 -04:00
SharedMemory.v SharedMemory: don't need exponentiation after all 2017-05-14 15:43:21 -04:00
SubsetTypes.v Working with Coq 8.5pl2 again 2017-11-18 11:45:26 -05:00
SubsetTypes_template.v SubsetTypes_template 2017-03-22 09:15:33 -04:00
TransitionSystems.v Fix typo in a comment 2017-02-27 09:52:21 -05:00
TransitionSystems_template.v Fix typo in a comment 2017-02-27 09:52:21 -05:00
TypesAndMutation.v Start of CompilerCorrectness: cfoldExprs_ok 2017-03-18 14:42:13 -04: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: DataAbstraction.v
  • Chapter 4: Interpreters.v
  • Chapter 5: TransitionSystems.v
    • IntroToProofScripting.v: writing scripts to find proofs in Coq
  • Chapter 6: ModelChecking.v
    • ProofByReflection.v: writing verified proof procedures in Coq
  • Chapter 7: OperationalSemantics.v
    • LogicProgramming.v: 'eauto' and friends, to automate proofs via logic programming
  • Chapter 8: AbstractInterpretation.v
  • Chapter 9: CompilerCorrectness.v
  • Chapter 10: LambdaCalculusAndTypeSoundness.v
  • Chapter 11: TypesAndMutation.v
  • Chapter 12: HoareLogic.v
  • Chapter 13: DeepAndShallowEmbeddings.v
  • Chapter 14: SeparationLogic.v
  • Chapter 15: SharedMemory.v
  • Chapter 16: ConcurrentSeparationLogic.v
  • Chapter 17: MessagesAndRefinement.v

There are also two supplementary files that are independent of the main narrative, for introducing programming with dependent types, a distinctive Coq feature that we neither use nor recommend for the problem sets, but which many students find interesting (and useful in other contexts).

  • SubsetTypes.v: a first introduction to dependent types by attaching predicates to normal types (used after CompilerCorrectness.v in the last course offering)
  • DependentInductiveTypes.v: building type dependency into datatype definitions (used after LambdaCalculusAndTypeSoundness.v in the last course offering)