Formal Reasoning About Programs
Coq TeX Other
Switch branches/tags
Nothing to show
Clone or download
achlipala Merge pull request #26 from bmsherman/book_typo
Fix typo in book with label for Embeddings chapter
Latest commit 79e5f91 May 29, 2018
Permalink
Failed to load latest commit information.
.gitignore Change ProofByReflection to work in Coq 8.6.1 Nov 18, 2017
AbstractInterpret.v Bump chapter numbers in Coq code comments Feb 21, 2017
AbstractInterpretation.v Increase precision of abstract subtraction for parity (thanks to Alek… Mar 20, 2018
BasicSyntax.v Push the last code change through a further copy-and-paste instance Feb 9, 2017
BasicSyntax_template.v Small typo fix in BasicSyntax Feb 7, 2017
CompilerCorrectness.v Proofreading CompilerCorrectness Mar 21, 2018
CompilerCorrectness_template.v Working again with Coq 8.6.1 Nov 18, 2017
ConcurrentSeparationLogic.v Proofreading ConcurrentSeparationLogic May 8, 2018
ConcurrentSeparationLogic_template.v Proofreading ConcurrentSeparationLogic May 8, 2018
Connecting.v Connecting chapter in LaTeX May 2, 2018
DataAbstraction.v Typo fixes Feb 26, 2018
DataAbstraction_template.v Typo fixes Feb 26, 2018
DeepAndShallowEmbeddings.v Proofreading DeepAndShallowEmbeddings Apr 22, 2018
DeepAndShallowEmbeddings_template.v Proofreading DeepAndShallowEmbeddings Apr 22, 2018
DeepInterp.ml DeepAndShallowEmbeddings: Deep Apr 10, 2016
DeeperInterp.ml DeepAndShallowEmbeddings: Deep Apr 10, 2016
DeeperWithFailInterp.ml DeepAndShallowEmbeddings: adding failure Apr 10, 2016
DependentInductiveTypes.v DependentInductiveTypes_template Apr 10, 2018
DependentInductiveTypes_template.v DependentInductiveTypes_template Apr 10, 2018
FirstClassFunctions.v FirstClassFunctions: comments Feb 20, 2018
FirstClassFunctions_template.v FirstClassFunctions_template Feb 20, 2018
Frap.v SubsetTypes Mar 21, 2017
FrapWithoutSets.v Improve robustness of set simplification Mar 17, 2018
HoareLogic.v minus notation should be for subtraction, not set minus Apr 26, 2018
HoareLogic_template.v minus notation should be for subtraction, not set minus Apr 26, 2018
Imp.v Add Imp, recapping OperationalSemantics object language and semantics Mar 4, 2016
Interpreters.v Merge Mar 19, 2017
Interpreters_template.v For Coq 8.5 compatibility, use [Admitted] instead of [admit] Feb 9, 2016
IntroToProofScripting.v Small improvements to IntroToProofScripting Feb 28, 2018
IntroToProofScripting_template.v Small improvements to IntroToProofScripting Feb 28, 2018
Invariant.v Connecting: proved an invariant for a compilation result Apr 29, 2018
LambdaCalculusAndTypeSoundness.v Revising LambdaCalculusAndTypeSoundness Apr 1, 2018
LambdaCalculusAndTypeSoundness_template.v Revising LambdaCalculusAndTypeSoundness Apr 1, 2018
LogicProgramming.v Proofreading LogicProgramming Mar 14, 2018
LogicProgramming_template.v Fix title in comments Mar 15, 2017
Makefile Add SepCancel to 'lib' target Apr 19, 2016
Map.v SubsetTypes Mar 21, 2017
MessagesAndRefinement.v SessionTypes: simplified and proved a key invariant May 13, 2018
ModelCheck.v SubsetTypes Mar 21, 2017
ModelChecking.v Some ModelChecking improvements Mar 5, 2018
ModelChecking_sol.v Tweak files for ModelChecking in class Mar 6, 2017
ModelChecking_template.v Fix up ModelChecking to track a change in TransitionSystems Mar 4, 2018
OperationalSemantics.v Bump chapter numbers in Coq code comments Feb 21, 2017
OperationalSemantics_template.v Tweak OperationalSemantics_template.v Mar 13, 2017
Polymorphism.v Revising Polymorphism Feb 12, 2018
Polymorphism_template.v Revising Polymorphism Feb 12, 2018
ProgramDerivation.v ProgramDerivation_template May 6, 2018
ProgramDerivation_template.v ProgramDerivation_template May 6, 2018
ProofByReflection.v ProofByReflection: some copyediting Mar 7, 2018
ProofByReflection_template.v ProofByReflection_template Mar 8, 2017
README.md Commented ProgramDerivation, with chapter renumbering in Coq code May 6, 2018
Relations.v SharedMemory: first optimization Apr 21, 2016
SepCancel.v Finalizing ConcurrentSeparationLogic May 1, 2016
SeparationLogic.v Proofreading SeparationLogic Apr 22, 2018
SeparationLogic_template.v Proofreading SeparationLogic Apr 22, 2018
SessionTypes.v SessionTypes: LaTeX finished May 15, 2018
Sets.v Improve robustness of set simplification Mar 17, 2018
SharedMemory.v Commented ProgramDerivation, with chapter renumbering in Coq code May 6, 2018
SubsetTypes.v Proofreading SubsetTypes Apr 3, 2018
SubsetTypes_template.v SubsetTypes_template Mar 22, 2017
TransitionSystems.v TransitionSystems: give more meaningful names to parallel trsys compo… Feb 21, 2018
TransitionSystems_template.v TransitionSystems: give more meaningful names to parallel trsys compo… Feb 21, 2018
TypesAndMutation.v Start of CompilerCorrectness: cfoldExprs_ok Mar 18, 2017
Var.v Interpreters: factorial example Feb 7, 2016
_CoqProject SessionTypes: commented May 13, 2018
frap_book.tex Fix typo in book with label for Embeddings chapter May 25, 2018
index.html 6.822 Spring 2018 Dec 18, 2017

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_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)