Skip to content

mkolosick/Software-Foundations-Exercises

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

15 Commits
Auto.v
Auto.v
 
 
Basics.v
Basics.v
 
 
Equiv.v
Equiv.v
 
 
Extraction.v
Extraction.v
 
 
Hoare.v
Hoare.v
 
 
Hoare2.v
Hoare2.v
 
 
HoareAsLogic.v
HoareAsLogic.v
 
 
HoareList.v
HoareList.v
 
 
Imp.v
Imp.v
 
 
ImpCEvalFun.v
ImpCEvalFun.v
 
 
ImpParser.v
ImpParser.v
 
 
Induction.v
Induction.v
 
 
LibTactics.v
LibTactics.v
 
 
Lists.v
Lists.v
 
 
Logic.v
Logic.v
 
 
MoreCoq.v
MoreCoq.v
 
 
MoreInd.v
MoreInd.v
 
 
MoreProp.v
MoreProp.v
 
 
MoreStlc.v
MoreStlc.v
 
 
Norm.v
Norm.v
 
 
PE.v
PE.v
 
 
Poly.v
Poly.v
 
 
ProofObjects.v
ProofObjects.v
 
 
Prop.v
Prop.v
 
 
README.md
README.md
 
 
RecordSub.v
RecordSub.v
 
 
Records.v
Records.v
 
 
References.v
References.v
 
 
Rel.v
Rel.v
 
 
Smallstep.v
Smallstep.v
 
 
StclProp.v
StclProp.v
 
 
Stlc.v
Stlc.v
 
 
Sub.v
Sub.v
 
 
Typechecking.v
Typechecking.v
 
 
Types.v
Types.v
 
 
UseAuto.v
UseAuto.v
 
 
UseTactics.v
UseTactics.v
 
 

Repository files navigation

Solutions to exercises in the Software Foundations textbook. Software Foundations teaches the Coq programming language, a dependently-typed, formal proof system and programming language.

The solutions are organized into files corresponding with Software Foundations' chapters.

About

Exercises in Software Foundations

Resources

Readme
Activity

Stars

6 stars

Watchers

2 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages