GitHub - jbujak/jafun: Separation logic for Jafun programming language, formalized in Coq

jbujak / jafun Public

Notifications You must be signed in to change notification settings
Fork 0
Star 0

Separation logic for Jafun programming language, formalized in Coq

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 120 Commits
.gitignore		.gitignore
JaChurch.v		JaChurch.v
JaChurchMeasure.v		JaChurchMeasure.v
JaEnvs.v		JaEnvs.v
JaEval.v		JaEval.v
JaIris.v		JaIris.v
JaIrisCommon.v		JaIrisCommon.v
JaIrisPermutation.v		JaIrisPermutation.v
JaIrisSoundness.v		JaIrisSoundness.v
JaProgram.v		JaProgram.v
JaProgramWf.v		JaProgramWf.v
JaRedInvariants.v		JaRedInvariants.v
JaSubtype.v		JaSubtype.v
JaSyntax.v		JaSyntax.v
JaTactics.v		JaTactics.v
JaTypes.v		JaTypes.v
JaUnique.v		JaUnique.v
JaUtils.v		JaUtils.v
Jafun.v		Jafun.v
Makefile.coq.conf		Makefile.coq.conf
README		README
_CoqProject		_CoqProject
fs_from_tfs.v		fs_from_tfs.v
fs_from_tfs2.v		fs_from_tfs2.v
fs_from_tfs3.v		fs_from_tfs3.v
logic.v		logic.v
proof-compute-average.sh		proof-compute-average.sh
proof-make-samples.sh		proof-make-samples.sh
tfs_exists.v		tfs_exists.v
tfs_exists2.v		tfs_exists2.v
tfs_exists3.v		tfs_exists3.v
tfs_exists4.v		tfs_exists4.v
tfs_exists5.v		tfs_exists5.v

Repository files navigation

Requirements:
* Coq 8.7.2
* Hammer
  http://cl-informatik.uibk.ac.at/cek/coqhammer/
  If you do not have it installed globally, you can
  create a subdirectory Hammer, compile (only Reconstr.vo is needed)
  and add the following line to the top of _CoqProject
  -R Hammer Hammer
  
[jjb] Przy przekompilowaniu `export COQBIN=/usr/bin/`