Formal Reasoning About Programs
Find a file
2020-04-21 19:22:39 -04:00
.gitignore Replace omega with lia 2020-02-08 14:41:07 -05:00
_CoqProject Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working 2020-02-10 13:44:35 -05:00
AbstractInterpret.v Prevent more warnings for Coq 8.10 2020-02-08 15:15:38 -05:00
AbstractInterpretation.v Increase precision of abstract subtraction for parity (thanks to Aleksejs Popovs for the suggestion) 2018-03-20 17:18:31 -04: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 Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working 2020-02-10 13:44:35 -05:00
CompilerCorrectness_template.v Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working 2020-02-10 13:44:35 -05:00
ConcurrentSeparationLogic.v Proofreading ConcurrentSeparationLogic 2018-05-08 09:13:06 -04:00
ConcurrentSeparationLogic_template.v Proofreading ConcurrentSeparationLogic 2018-05-08 09:13:06 -04:00
Connecting.v Connecting chapter in LaTeX 2018-05-02 14:13:26 -04:00
DataAbstraction.v Typo fixes 2018-02-25 19:40:10 -05:00
DataAbstraction_template.v Typo fixes 2018-02-25 19:40:10 -05:00
DeepAndShallowEmbeddings.v First phase of update for Coq 8.10 2020-02-02 17:16:19 -05:00
DeepAndShallowEmbeddings_template.v First phase of update for Coq 8.10 2020-02-02 17:16:19 -05: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 Merge 2020-02-02 17:19:40 -05:00
DependentInductiveTypes_template.v Merge 2020-02-02 17:19:40 -05:00
FirstClassFunctions.v A little more text for the new FirstClassFunctions examples 2020-02-15 12:32:36 -05:00
FirstClassFunctions_template.v Update FirstClassFunctions_template from new source material 2020-02-12 14:03:15 -05:00
Frap.v SubsetTypes 2017-03-21 19:27:36 -04:00
frap_book.tex Truly building with Coq 8.9 again 2020-02-10 13:53:26 -05:00
FrapWithoutSets.v Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working 2020-02-10 13:44:35 -05:00
HoareLogic.v Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working 2020-02-10 13:44:35 -05:00
HoareLogic_template.v minus notation should be for subtraction, not set minus 2018-04-25 22:28:22 -04:00
Imp.v Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working 2020-02-10 13:44:35 -05:00
index.html Link to Spring 2020 users of the book 2020-02-08 10:46:47 -05:00
Interpreters.v Truly building with Coq 8.9 again 2020-02-10 13:53:26 -05:00
Interpreters_template.v Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working 2020-02-10 13:44:35 -05:00
IntroToProofScripting.v Small improvements to IntroToProofScripting 2018-02-28 09:01:07 -05:00
IntroToProofScripting_template.v Small improvements to IntroToProofScripting 2018-02-28 09:01:07 -05:00
Invariant.v Connecting: proved an invariant for a compilation result 2018-04-29 16:57:47 -04:00
LambdaCalculusAndTypeSoundness.v Revising LambdaCalculusAndTypeSoundness 2018-04-01 13:06:47 -04:00
LambdaCalculusAndTypeSoundness_template.v Revising LambdaCalculusAndTypeSoundness 2018-04-01 13:06:47 -04:00
LogicProgramming.v Proofreading LogicProgramming 2018-03-13 20:26:17 -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 Prevent more warnings for Coq 8.10 2020-02-08 15:15:38 -05:00
MessagesAndRefinement.v fix warnings in MessagesAndRefinement.v 2020-04-21 19:22:39 -04:00
ModelCheck.v Prevent more warnings for Coq 8.10 2020-02-08 15:15:38 -05:00
ModelChecking.v Some ModelChecking improvements 2018-03-04 19:23:36 -05:00
ModelChecking_sol.v Tweak files for ModelChecking in class 2017-03-06 09:44:29 -05:00
ModelChecking_template.v Fix up ModelChecking to track a change in TransitionSystems 2018-03-04 18:46:12 -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 Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working 2020-02-10 13:44:35 -05:00
Polymorphism_template.v Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working 2020-02-10 13:44:35 -05:00
ProgramDerivation.v ProgramDerivation_template 2018-05-06 19:49:10 -04:00
ProgramDerivation_template.v ProgramDerivation_template 2018-05-06 19:49:10 -04:00
ProofByReflection.v First phase of update for Coq 8.10 2020-02-02 17:16:19 -05:00
ProofByReflection_template.v First phase of update for Coq 8.10 2020-02-02 17:16:19 -05:00
README.md Commented ProgramDerivation, with chapter renumbering in Coq code 2018-05-06 12:53:49 -04:00
Relations.v Prevent more warnings for Coq 8.10 2020-02-08 15:15:38 -05:00
SeparationLogic.v Proofreading SeparationLogic 2018-04-22 14:32:38 -04:00
SeparationLogic_template.v Proofreading SeparationLogic 2018-04-22 14:32:38 -04:00
SepCancel.v Finalizing ConcurrentSeparationLogic 2016-05-01 19:45:51 -04:00
SessionTypes.v SessionTypes: LaTeX finished 2018-05-15 15:27:57 -04:00
Sets.v Prevent more warnings for Coq 8.10 2020-02-08 15:15:38 -05:00
SharedMemory.v First phase of update for Coq 8.10 2020-02-02 17:16:19 -05:00
SubsetTypes.v Proofreading SubsetTypes 2018-04-03 18:32:56 -04:00
SubsetTypes_template.v SubsetTypes_template 2017-03-22 09:15:33 -04:00
TransitionSystems.v TransitionSystems: give more meaningful names to parallel trsys components 2018-02-21 16:45:15 -05:00
TransitionSystems_template.v TransitionSystems: give more meaningful names to parallel trsys components 2018-02-21 16:45:15 -05:00
TypesAndMutation.v Replace omega with lia 2020-02-08 14:41:07 -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: DataAbstraction.v
  • Chapter 4: Interpreters.v
    • FirstClassFunctions.v: functions as data; continuations and continuation-passing style
  • 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: Connecting.v
  • Chapter 16: ProgramDerivation.v
  • Chapter 17: SharedMemory.v
  • Chapter 18: ConcurrentSeparationLogic.v
  • Chapter 19: 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)