Formal Reasoning About Programs
Find a file
Adam Chlipala 2ef93d36fc Typo fix
2023-02-19 13:42:53 -05:00
.gitignore Separate out library code with its own license 2020-03-17 09:22:06 -04:00
_CoqProject EvaluationContexts_template 2021-03-30 16:12:37 -04:00
_CoqProject.fraplib Separate out library code with its own license 2020-03-17 09:22:06 -04:00
AbstractInterpret.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
AbstractInterpretation.v Update AbstractInterpretation for newer Coq versions 2022-02-06 13:13:29 -05:00
BasicSyntax.v Revising for next lecture 2022-01-29 16:28:31 -05:00
BasicSyntax_template.v Small typo fix in BasicSyntax 2017-02-07 15:11:54 -05:00
CompilerCorrectness.v Revising for tomorrow's lecture 2022-03-06 14:10:06 -05:00
CompilerCorrectness_template.v Revising before class 2021-03-21 10:14:31 -04:00
ConcurrentSeparationLogic.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
ConcurrentSeparationLogic_template.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
Connecting.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
DataAbstraction.v Revising for Wednesday's lecture 2022-02-20 12:29:17 -05:00
DataAbstraction_template.v Ported to Coq 8.15 2022-01-29 15:13:09 -05:00
DeepAndShallowEmbeddings.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
DeepAndShallowEmbeddings_template.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
DeeperInterp.ml Revising before class 2020-04-08 10:48:14 -04:00
DeeperWithFailInterp.ml Revising before class 2020-04-08 10:48:14 -04:00
DeepInterp.ml Revising before class 2020-04-08 10:48:14 -04:00
DependentInductiveTypes.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
DependentInductiveTypes_template.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
EvaluationContexts.v EvaluationContexts: exceptions 2021-03-28 15:33:23 -04:00
EvaluationContexts_template.v EvaluationContexts_template 2021-03-30 16:12:37 -04:00
FirstClassFunctions.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -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 Revising for Wednesday's lecture 2022-04-18 12:58:53 -04:00
FrapWithoutSets.v Update cases tactic to work on N type 2022-02-06 12:47:50 -05:00
HoareLogic.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
HoareLogic_template.v Merge pull request #55 from cpitclaudel/hoare_tweaks 2021-04-12 16:01:44 -04:00
Imp.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
index.html Latest MIT offering finished 2022-08-21 08:59:23 -04:00
Interpreters.v Revising for tomorrow's lecture 2022-02-06 12:35:54 -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 Typo fix 2023-02-19 13:42:53 -05:00
IntroToProofScripting_template.v Revising for next lecture 2021-03-07 14:21:30 -05:00
Invariant.v Connecting: proved an invariant for a compilation result 2018-04-29 16:57:47 -04:00
LambdaCalculusAndTypeSoundness.v Revising for tomorrow's lecture 2022-03-13 18:10:19 -04:00
LambdaCalculusAndTypeSoundness_template.v Revising for tomorrow's lecture 2022-03-13 18:10:19 -04:00
LICENSE Separate out library code with its own license 2020-03-17 09:22:06 -04:00
LogicProgramming.v Revising before tomorrow's lecture 2021-03-16 18:23:24 -04:00
LogicProgramming_template.v Revising before tomorrow's lecture 2021-03-16 18:23:24 -04:00
Makefile Separate out library code with its own license 2020-03-17 09:22:06 -04:00
Makefile.fraplib Separate out library code with its own license 2020-03-17 09:22:06 -04:00
Map.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
MessagesAndRefinement.v Revising for the final week of class 2021-05-16 11:55:01 -04:00
ModelCheck.v Revising before class, including with an optimization to the model-checking engine 2020-04-20 11:56:23 -04:00
ModelChecking.v Revising for Tuesday's lecture 2022-02-20 12:02:38 -05:00
ModelChecking_sol.v Tweak files for ModelChecking in class 2017-03-06 09:44:29 -05:00
ModelChecking_template.v Revising for Tuesday's lecture 2022-02-20 12:02:38 -05:00
OperationalSemantics.v Revising for Monday's lecture 2022-02-26 15:58:03 -05:00
OperationalSemantics_template.v Revising for Monday's lecture 2022-02-26 15:58:03 -05:00
Polymorphism.v Revising for next next lecture 2022-01-29 17:22:33 -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 Ported to Coq 8.15 2022-01-29 15:13:09 -05:00
ProgramDerivation_template.v Revising before this week's lectures 2021-05-10 10:45:34 -04:00
ProofByReflection.v Revising for Wednesday's lecture 2022-03-06 14:47:05 -05:00
ProofByReflection_template.v Revising for Wednesday's lecture 2022-03-06 14:47:05 -05:00
README.md Update code index with this semester's chapter additions 2021-05-19 17:01:51 -04:00
Relations.v Prevent more warnings for Coq 8.10 2020-02-08 15:15:38 -05:00
RuleInduction.v Revising for Wednesday's lecture 2022-02-06 13:03:43 -05:00
RuleInduction_template.v Change notation to remain compatible with multiple Coq versions 2022-01-31 21:02:31 -05:00
SeparationLogic.v Revising for next Wednesday's lecture 2022-04-03 14:40:20 -04:00
SeparationLogic_template.v Revising for next Wednesday's lecture 2022-04-03 14:40:20 -04:00
SepCancel.v A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
SessionTypes.v Revising for the final week of class 2021-05-16 11:55:01 -04:00
Sets.v Prevent more warnings for Coq 8.10 2020-02-08 15:15:38 -05:00
SharedMemory.v Revising for Wednesday's lecture 2022-04-18 12:58:53 -04:00
SubsetTypes.v Revising for this week's lectures 2022-03-27 13:40:08 -04:00
SubsetTypes_template.v Revising for this week's lectures 2022-03-27 13:40:08 -04:00
TransitionSystems.v Revising for tomorrow's lecture 2022-02-13 14:16:33 -05:00
TransitionSystems_template.v More cleanup around addition of RuleInduction 2021-03-01 12:15:34 -05:00
TypesAndMutation.v Revising for this week's lectures 2022-03-27 13:40:08 -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
    • FirstClassFunctions.v: functions as data; continuations and continuation-passing style
  • Chapter 5: RuleInduction.v
  • Chapter 6: TransitionSystems.v
    • IntroToProofScripting.v: writing scripts to find proofs in Coq
  • Chapter 7: ModelChecking.v
    • ProofByReflection.v: writing verified proof procedures in Coq
  • Chapter 8: OperationalSemantics.v
    • LogicProgramming.v: 'eauto' and friends, to automate proofs via logic programming
  • Chapter 9: AbstractInterpretation.v
  • Chapter 10: CompilerCorrectness.v
  • Chapter 11: LambdaCalculusAndTypeSoundness.v
  • Chapter 12: EvaluationContexts.v
  • Chapter 13: TypesAndMutation.v
  • Chapter 14: HoareLogic.v
  • Chapter 15: DeepAndShallowEmbeddings.v
  • Chapter 16: SeparationLogic.v
  • Chapter 17: Connecting.v
  • Chapter 18: ProgramDerivation.v
  • Chapter 19: SharedMemory.v
  • Chapter 20: ConcurrentSeparationLogic.v
  • Chapter 21: MessagesAndRefinement.v
  • Chapter 22: SessionTypes.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)