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)

Name	Name	Last commit message
Latest commit History 578 Commits
.gitignore	.gitignore
AbstractInterpret.v	AbstractInterpret.v
AbstractInterpretation.v	AbstractInterpretation.v
BasicSyntax.v	BasicSyntax.v
BasicSyntax_template.v	BasicSyntax_template.v
CompilerCorrectness.v	CompilerCorrectness.v
CompilerCorrectness_template.v	CompilerCorrectness_template.v
ConcurrentSeparationLogic.v	ConcurrentSeparationLogic.v
ConcurrentSeparationLogic_template.v	ConcurrentSeparationLogic_template.v
Connecting.v	Connecting.v
DataAbstraction.v	DataAbstraction.v
DataAbstraction_template.v	DataAbstraction_template.v
DeepAndShallowEmbeddings.v	DeepAndShallowEmbeddings.v
DeepAndShallowEmbeddings_template.v	DeepAndShallowEmbeddings_template.v
DeepInterp.ml	DeepInterp.ml
DeeperInterp.ml	DeeperInterp.ml
DeeperWithFailInterp.ml	DeeperWithFailInterp.ml
DependentInductiveTypes.v	DependentInductiveTypes.v
DependentInductiveTypes_template.v	DependentInductiveTypes_template.v
EvaluationContexts.v	EvaluationContexts.v
EvaluationContexts_template.v	EvaluationContexts_template.v
FirstClassFunctions.v	FirstClassFunctions.v
FirstClassFunctions_template.v	FirstClassFunctions_template.v
Frap.v	Frap.v
FrapWithoutSets.v	FrapWithoutSets.v
HoareLogic.v	HoareLogic.v
HoareLogic_template.v	HoareLogic_template.v
Imp.v	Imp.v
Interpreters.v	Interpreters.v
Interpreters_template.v	Interpreters_template.v
IntroToProofScripting.v	IntroToProofScripting.v
IntroToProofScripting_template.v	IntroToProofScripting_template.v
Invariant.v	Invariant.v
LICENSE	LICENSE
LambdaCalculusAndTypeSoundness.v	LambdaCalculusAndTypeSoundness.v
LambdaCalculusAndTypeSoundness_template.v	LambdaCalculusAndTypeSoundness_template.v
LogicProgramming.v	LogicProgramming.v
LogicProgramming_template.v	LogicProgramming_template.v
Makefile	Makefile
Makefile.fraplib	Makefile.fraplib
Map.v	Map.v
MessagesAndRefinement.v	MessagesAndRefinement.v
ModelCheck.v	ModelCheck.v
ModelChecking.v	ModelChecking.v
ModelChecking_sol.v	ModelChecking_sol.v
ModelChecking_template.v	ModelChecking_template.v
OperationalSemantics.v	OperationalSemantics.v
OperationalSemantics_template.v	OperationalSemantics_template.v
Polymorphism.v	Polymorphism.v
Polymorphism_template.v	Polymorphism_template.v
ProgramDerivation.v	ProgramDerivation.v
ProgramDerivation_template.v	ProgramDerivation_template.v
ProofByReflection.v	ProofByReflection.v
ProofByReflection_template.v	ProofByReflection_template.v
README.md	README.md
Relations.v	Relations.v
RuleInduction.v	RuleInduction.v
RuleInduction_template.v	RuleInduction_template.v
SepCancel.v	SepCancel.v
SeparationLogic.v	SeparationLogic.v
SeparationLogic_template.v	SeparationLogic_template.v
SessionTypes.v	SessionTypes.v
Sets.v	Sets.v
SharedMemory.v	SharedMemory.v
SubsetTypes.v	SubsetTypes.v
SubsetTypes_template.v	SubsetTypes_template.v	8000
TransitionSystems.v	TransitionSystems.v
TransitionSystems_template.v	TransitionSystems_template.v
TypesAndMutation.v	TypesAndMutation.v
Var.v	Var.v
_CoqProject	_CoqProject
_CoqProject.fraplib	_CoqProject.fraplib
frap_book.tex	frap_book.tex
index.html	index.html

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Repository files navigation

Formal Reasoning About Programs

Code associated with the different chapters

About

Releases

Packages

Languages

Latest commit

History

Repository files navigation

Formal Reasoning About Programs

Code associated with the different chapters