Skip to content
/ coq Public
forked from rabimba/coq

My Experiments with coq

0 stars 2 forks Branches Tags Activity
Star
Notifications You must be signed in to change notification settings

jc-su/coq

BranchesTags
 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

6 Commits
.gitattributes
.gitattributes
 
 
.gitignore
.gitignore
 
 
2nd day.v
2nd day.v
 
 
AVLProof.v
AVLProof.v
 
 
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
 
 
Induction_2.v
Induction_2.v
 
 
Induction_alternate4drhamlen.v
Induction_alternate4drhamlen.v
 
 
LibTactics.v
LibTactics.v
 
 
Lists.v
Lists.v
 
 
Lists.vo
Lists.vo
 
 
Logic.v
Logic.v
 
 
MoreCoq.v
MoreCoq.v
 
 
MoreCoq.vo
MoreCoq.vo
 
 
MoreInd.v
MoreInd.v
 
 
MoreProp.v
MoreProp.v
 
 
MoreStlc.v
MoreStlc.v
 
 
Norm.v
Norm.v
 
 
PE.v
PE.v
 
 
Poly.v
Poly.v
 
 
Postscript.v
Postscript.v
 
 
Preface.v
Preface.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
 
 
SfLib.v
SfLib.v
 
 
Smallstep.v
Smallstep.v
 
 
Stlc.v
Stlc.v
 
 
StlcProp.v
StlcProp.v
 
 
Sub.v
Sub.v
 
 
Symbols.v
Symbols.v
 
 
Typechecking.v
Typechecking.v
 
 
Types.v
Types.v
 
 
UseAuto.v
UseAuto.v
 
 
UseTactics.v
UseTactics.v
 
 
andb3.v
andb3.v
 
 
m less than n.v
m less than n.v
 
 
nandb.v
nandb.v
 
 

Repository files navigation

coq

==========

Description

Coq is an interactive theorem prover.

These files are assignments and their solutions (my interpretation) for the course by Kevin Hamlin in UTD F13.

How to use??

Use either coqide or coq proof assistant to load these. Alternatively if you are using linux use a compatible editor (emacs) with proper plugins to make it work.

AVLTree

The AVL Tree proof is the final project for the course. The proof is not efficient (as discussed with Dr. Hamlen) but atleast we managed to prove the tree.

About

My Experiments with coq

Resources

Readme
Activity

Stars

0 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages

  • Coq 98.3%
  • Verilog 1.7%