GitHub - alxest/Software-Foundations

This branch is 10 commits ahead of sven--/Software-Foundations:master.

Name	Name	Last commit message	Last commit date
Latest commit alxest Implement ImpCEvalFun.v. Dec 14, 2015 d11014e · Dec 14, 2015 History 41 Commits
.depend	.depend	inital commit	Jul 1, 2014
.gitignore	.gitignore	Update gitignore.	Jun 30, 2015
Auto.html	Auto.html	inital commit	Jul 1, 2014
Auto.v	Auto.v	Auto.v done.	Jul 27, 2014
Basics.html	Basics.html	inital commit	Jul 1, 2014
Basics.v	Basics.v	induction.v done, except 1 problem	Jul 3, 2014
Equiv.html	Equiv.html	inital commit	Jul 1, 2014
Equiv.v	Equiv.v	Equiv.v done, excluded "For" loop addition from Imp.v, therefore skip…	Jul 17, 2014
Extraction.html	Extraction.html	inital commit	Jul 1, 2014
Extraction.v	Extraction.v	inital commit	Jul 1, 2014
Hoare.html	Hoare.html	inital commit	Jul 1, 2014
Hoare.v	Hoare.v	Hoare.v done.	Jul 21, 2014
Hoare2.html	Hoare2.html	inital commit	Jul 1, 2014
Hoare2.v	Hoare2.v	Hoare2.v done.	Jul 24, 2014
HoareAsLogic.html	HoareAsLogic.html	Introduced ommitted files.	Jul 17, 2014
HoareAsLogic.v	HoareAsLogic.v	Introduced ommitted files.	Jul 17, 2014
Imp.html	Imp.html	inital commit	Jul 1, 2014
Imp.v	Imp.v	Equiv.v done, excluded "For" loop addition from Imp.v, therefore skip…	Jul 17, 2014
ImpCEvalFun.html	ImpCEvalFun.html	inital commit	Jul 1, 2014
ImpCEvalFun.v	ImpCEvalFun.v	Implement ImpCEvalFun.v.	Dec 14, 2015
ImpParser.html	ImpParser.html	inital commit	Jul 1, 2014
ImpParser.v	ImpParser.v	inital commit	Jul 1, 2014
Induction.html	Induction.html	inital commit	Jul 1, 2014
Induction.v	Induction.v	induction.v done, except 1 problem	Jul 3, 2014
LICENSE	LICENSE	inital commit	Jul 1, 2014
LibTactics.html	LibTactics.html	Introduced ommitted files.	Jul 17, 2014
LibTactics.v	LibTactics.v	Introduced ommitted files.	Jul 17, 2014
Lists.html	Lists.html	inital commit	Jul 1, 2014
Lists.v	Lists.v	lists.v done.	Jul 3, 2014
Logic.html	Logic.html	inital commit	Jul 1, 2014
Logic.v	Logic.v	Class works in Logic.v	Nov 25, 2015
Makefile	Makefile	inital commit	Jul 1, 2014
MoreCoq.html	MoreCoq.html	inital commit	Jul 1, 2014
MoreCoq.v	MoreCoq.v	MoreCoq done, without 2 problems.	Jul 5, 2014
MoreInd.html	MoreInd.html	inital commit	Jul 1, 2014
MoreInd.v	MoreInd.v	Class works in Logic.v	Nov 25, 2015
MoreLogic.html	MoreLogic.html	inital commit	Jul 1, 2014
MoreLogic.v	MoreLogic.v	MoreLogic.v done, except pigeonhole	Jul 12, 2014
MoreStlc.html	MoreStlc.html	inital commit	Jul 1, 2014
MoreStlc.v	MoreStlc.v	MoreStlc.v, added "soundness"	Aug 6, 2014
Norm.html	Norm.html	Introduced ommitted files.	Jul 17, 2014
Norm.v	Norm.v	Introduced ommitted files.	Jul 17, 2014
PE.html	PE.html	Introduced ommitted files.	Jul 17, 2014
PE.v	PE.v	Introduced ommitted files.	Jul 17, 2014
Poly.html	Poly.html	inital commit	Jul 1, 2014
Poly.v	Poly.v	added omitted proof.	Jul 5, 2014
Postscript.html	Postscript.html	Introduced ommitted files.	Jul 17, 2014
Postscript.v	Postscript.v	Introduced ommitted files.	Jul 17, 2014
Preface.html	Preface.html	inital commit	Jul 1, 2014
Preface.v	Preface.v	inital commit	Jul 1, 2014
ProofObjects.html	ProofObjects.html	inital commit	Jul 1, 2014
ProofObjects.v	ProofObjects.v	Update ProofObjects.v.	Dec 3, 2015
Prop.html	Prop.html	inital commit	Jul 1, 2014
Prop.v	Prop.v	Poly.v done, except Admitted in lisist_step_induction	Jul 9, 2014
RecordSub.html	RecordSub.html	Introduced ommitted files.	Jul 17, 2014
RecordSub.v	RecordSub.v	Introduced ommitted files.	Jul 17, 2014
Records.html	Records.html	Introduced ommitted files.	Jul 17, 2014
Records.v	Records.v	Records.v done, not following suggested dependency	Aug 16, 2014
References.html	References.html	Introduced ommitted files.	Jul 17, 2014
References.v	References.v	References.v done, except garbage_collector	Aug 13, 2014
Rel.html	Rel.html	Introduced ommitted files.	Jul 17, 2014
Rel.v	Rel.v	Rel.v done	Sep 19, 2014
Review1.html	Review1.html	inital commit	Jul 1, 2014
Review1.v	Review1.v	inital commit	Jul 1, 2014
Review2.html	Review2.html	inital commit	Jul 1, 2014
Review2.v	Review2.v	inital commit	Jul 1, 2014
SfLib.html	SfLib.html	inital commit	Jul 1, 2014
SfLib.v	SfLib.v	inital commit	Jul 1, 2014
Smallstep.html	Smallstep.html	inital commit	Jul 1, 2014
Smallstep.v	Smallstep.v	Smallstep.v done.	Jul 26, 2014
Stlc.html	Stlc.html	inital commit	Jul 1, 2014
Stlc.v	Stlc.v	Stlc.v done.	Jul 31, 2014
StlcProp.html	StlcProp.html	inital commit	Jul 1, 2014
StlcProp.v	StlcProp.v	Fix broken scripts in 8.4pl5	Nov 26, 2015
Sub.html	Sub.html	inital commit	Jul 1, 2014
Sub.v	Sub.v	Sub.v done, skipped "variations"	Aug 17, 2014
Symbols.html	Symbols.html	inital commit	Jul 1, 2014
Symbols.v	Symbols.v	inital commit	Jul 1, 2014
Typechecking.html	Typechecking.html	Introduced ommitted files.	Jul 17, 2014
Typechecking.v	Typechecking.v	Typechecking.v done.	Aug 6, 2014
Types.html	Types.html	inital commit	Jul 1, 2014
Types.v	Types.v	Types.v done.	Jul 29, 2014
UseAuto.html	UseAuto.html	Introduced ommitted files.	Jul 17, 2014
UseAuto.v	UseAuto.v	Introduced ommitted files.	Jul 17, 2014
UseTactics.html	UseTactics.html	Introduced ommitted files.	Jul 17, 2014
UseTactics.v	UseTactics.v	Introduced ommitted files.	Jul 17, 2014
coqdoc.css	coqdoc.css	inital commit	Jul 1, 2014
coqindex.html	coqindex.html	inital commit	Jul 1, 2014
deps.gif	deps.gif	inital commit	Jul 1, 2014
deps.html	deps.html	inital commit	Jul 1, 2014
deps.map	deps.map	inital commit	Jul 1, 2014
imp1.ml	imp1.ml	inital commit	Jul 1, 2014
imp1.mli	imp1.mli	inital commit	Jul 1, 2014
imp2.mli	imp2.mli	inital commit	Jul 1, 2014
impdriver.ml	impdriver.ml	inital commit	Jul 1, 2014
index-bg.jpg	index-bg.jpg	inital commit	Jul 1, 2014
index.html	index.html	inital commit	Jul 1, 2014
jquery-1.8.3.js	jquery-1.8.3.js	inital commit	Jul 1, 2014
jquery.maphilight.min.js	jquery.maphilight.min.js	inital commit	Jul 1, 2014
main.js	main.js	inital commit	Jul 1, 2014
normdriver.ml	normdriver.ml	inital commit	Jul 1, 2014
slides.js	slides.js	inital commit	Jul 1, 2014
toc.html	toc.html	inital commit	Jul 1, 2014

Repository files navigation

Copyright (c) 2012

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.