GitHub - nunzioc/softwarefoundations

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 6 Commits
common		common
#Basics.v#		#Basics.v#
#Lists.v#		#Lists.v#
.Basics.aux		.Basics.aux
.BasicsTest.aux		.BasicsTest.aux
.Induction.aux		.Induction.aux
.Preface.aux		.Preface.aux
.coqdeps.d		.coqdeps.d
Auto.html		Auto.html
Auto.v		Auto.v
AutoTest.v		AutoTest.v
Basics.glob		Basics.glob
Basics.html		Basics.html
Basics.v		Basics.v
Basics.vo		Basics.vo
Basics.v~		Basics.v~
BasicsTest.glob		BasicsTest.glob
BasicsTest.v		BasicsTest.v
BasicsTest.vo		BasicsTest.vo
Bib.html		Bib.html
Bib.v		Bib.v
BibTest.v		BibTest.v
Extraction.html		Extraction.html
Extraction.v		Extraction.v
ExtractionTest.v		ExtractionTest.v
Imp.html		Imp.html
Imp.v		Imp.v
ImpCEvalFun.html		ImpCEvalFun.html
ImpCEvalFun.v		ImpCEvalFun.v
ImpCEvalFunTest.v		ImpCEvalFunTest.v
ImpParser.html		ImpParser.html
ImpParser.v		ImpParser.v
ImpParserTest.v		ImpParserTest.v
ImpTest.v		ImpTest.v
IndPrinciples.html		IndPrinciples.html
IndPrinciples.v		IndPrinciples.v
IndPrinciplesTest.v		IndPrinciplesTest.v
IndProp.html		IndProp.html
IndProp.v		IndProp.v
IndPropTest.v		IndPropTest.v
Induction.glob		Induction.glob
Induction.html		Induction.html
Induction.v		Induction.v
Induction.vo		Induction.vo
InductionTest.v		InductionTest.v
LICENSE		LICENSE
Lists.html		Lists.html
Lists.v		Lists.v
ListsTest.v		ListsTest.v
Logic.html		Logic.html
Logic.v		Logic.v
LogicTest.v		LogicTest.v
Makefile		Makefile
Makefile.conf		Makefile.conf
Maps.html		Maps.html
Maps.v		Maps.v
MapsTest.v		MapsTest.v
Poly.html		Poly.html
Poly.v		Poly.v
PolyTest.v		PolyTest.v
Postscript.html		Postscript.html
Postscript.v		Postscript.v
PostscriptTest.v		PostscriptTest.v
Preface.glob		Preface.glob
Preface.html		Preface.html
Preface.v		Preface.v
Preface.vo		Preface.vo
PrefaceTest.v		PrefaceTest.v
ProofObjects.html		ProofObjects.html
ProofObjects.v		ProofObjects.v
ProofObjectsTest.v		ProofObjectsTest.v
README		README
Rel.html		Rel.html
Rel.v		Rel.v
RelTest.v		RelTest.v
Tactics.html		Tactics.html
Tactics.v		Tactics.v
TacticsTest.v		TacticsTest.v
_CoqProject		_CoqProject
coqindex.html		coqindex.html
deps.gif		deps.gif
deps.html		deps.html
deps.map		deps.map
imp.ml		imp.ml
imp.mli		imp.mli
imp1.ml		imp1.ml
imp1.mli		imp1.mli
imp2.ml		imp2.ml
imp2.mli		imp2.mli
impdriver.ml		impdriver.ml
index.html		index.html
toc.html		toc.html

Repository files navigation

This repo contains my solutions for problems from Software Foundatations 
(https://softwarefoundations.cis.upenn.edu). It's a course that teaches the
fundamentals of proofs and logic using the Coq proof assistent.

So far I have solved.
- Basics
- Induction
- Lists
- Polymorphism and Higher Order Functions