GitHub - renan061/elo-coq: Formalization of the Elo language in Coq alongside a proof that the language is free from data races.

renan061 / elo-coq Public

Formalization of the Elo language in Coq alongside a proof that the language is free from data races.

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 280 Commits
.gitignore		.gitignore
Array.v		Array.v
ConsistentRegions.v		ConsistentRegions.v
ConsistentTerm.v		ConsistentTerm.v
ConsistentWaits.v		ConsistentWaits.v
Core.v		Core.v
Eval.v		Eval.v
Examples.v		Examples.v
Exclusivity.v		Exclusivity.v
GCR.v		GCR.v
HappensBefore.v		HappensBefore.v
HasVar.v		HasVar.v
Holding.v		Holding.v
InheritanceNoCR.v		InheritanceNoCR.v
InheritanceNoInit.v		InheritanceNoInit.v
InheritanceNoReacq.v		InheritanceNoReacq.v
Invariants.v		Invariants.v
Kappa.v		Kappa.v
Keywords.v		Keywords.v
Makefile		Makefile
Map.v		Map.v
MutualExclusion.v		MutualExclusion.v
NoCR.v		NoCR.v
NoInit.v		NoInit.v
NoReacq.v		NoReacq.v
NoRef.v		NoRef.v
NoUninitRefs.v		NoUninitRefs.v
NoWRef.v		NoWRef.v
OneCR.v		OneCR.v
OneInit.v		OneInit.v
PointerTypes.v		PointerTypes.v
SafeTerm.v		SafeTerm.v
Safety.v		Safety.v
SafetyLemmas.v		SafetyLemmas.v
SafetyUtil.v		SafetyUtil.v
Sem.v		Sem.v
SemExt.v		SemExt.v
Soundness.v		Soundness.v
SyntacticProperties.v		SyntacticProperties.v
TypeProperties.v		TypeProperties.v
UniqueInits.v		UniqueInits.v
Upsilon.v		Upsilon.v
Util.v		Util.v
ValidTerm.v		ValidTerm.v
Values.v		Values.v
Waiting.v		Waiting.v
WellTypedTerm.v		WellTypedTerm.v
_CoqProject		_CoqProject
elo-coq-v1.zip		elo-coq-v1.zip