GitHub - Alasdair/SKAT: An Isabelle implementation of Dexter Kozen's schematic Kleene algebra + Hoare logic.

Alasdair / SKAT Public

An Isabelle implementation of Dexter Kozen's schematic Kleene algebra + Hoare logic.

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 10 Commits
generated		generated
Base.thy		Base.thy
Boolean_Algebra_Extras.thy		Boolean_Algebra_Extras.thy
Dioid.thy		Dioid.thy
Galois_Connection.thy		Galois_Connection.thy
IsaMakefile		IsaMakefile
KAT.thy		KAT.thy
KAT_Module.thy		KAT_Module.thy
Kleene_Algebra.thy		Kleene_Algebra.thy
Kozen_Example.thy		Kozen_Example.thy
Lattice.thy		Lattice.thy
ROOT.ML		ROOT.ML
SKAT.thy		SKAT.thy
SKAT_Euclid.thy		SKAT_Euclid.thy
SKAT_Eval.thy		SKAT_Eval.thy
SKAT_Tactics.thy		SKAT_Tactics.thy
SKAT_Term.thy		SKAT_Term.thy
Set_Model.thy		Set_Model.thy
compile.sh		compile.sh
isabelle.sty		isabelle.sty
isabellesym.sty		isabellesym.sty
llncs.cls		llncs.cls
llncs.dem		llncs.dem
llncs.ind		llncs.ind
paper.bib		paper.bib
paper.tex		paper.tex
pdfsetup.sty		pdfsetup.sty
railsetup.sty		railsetup.sty