GitHub - epfl-systemf/sepviz-software-foundations-slf

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 42 Commits
.vscode		.vscode
.envrc		.envrc
.gitignore		.gitignore
Affine.v		Affine.v
Arrays.v		Arrays.v
Basic.v		Basic.v
Bib.v		Bib.v
Himpl.v		Himpl.v
Hprop.v		Hprop.v
LICENSE		LICENSE
LibAxioms.v		LibAxioms.v
LibBool.v		LibBool.v
LibChoice.v		LibChoice.v
LibContainer.v		LibContainer.v
LibCore.v		LibCore.v
LibEpsilon.v		LibEpsilon.v
LibEqual.v		LibEqual.v
LibFun.v		LibFun.v
LibInt.v		LibInt.v
LibList.v		LibList.v
LibListExec.v		LibListExec.v
LibListZ.v		LibListZ.v
LibLogic.v		LibLogic.v
LibMin.v		LibMin.v
LibMonoid.v		LibMonoid.v
LibMultiset.v		LibMultiset.v
LibNat.v		LibNat.v
LibOperation.v		LibOperation.v
LibOption.v		LibOption.v
LibOrder.v		LibOrder.v
LibProd.v		LibProd.v
LibReflect.v		LibReflect.v
LibRelation.v		LibRelation.v
LibSepFmap.v		LibSepFmap.v
LibSepMinimal.v		LibSepMinimal.v
LibSepReference.v		LibSepReference.v
LibSepSimpl.v		LibSepSimpl.v
LibSepTLCbuffer.v		LibSepTLCbuffer.v
LibSepVar.v		LibSepVar.v
LibSet.v		LibSet.v
LibString.v		LibString.v
LibSum.v		LibSum.v
LibTactics.v		LibTactics.v
LibUnit.v		LibUnit.v
LibWf.v		LibWf.v
Makefile		Makefile
Nondet.v		Nondet.v
Partial.v		Partial.v
Postscript.v		Postscript.v
Preface.v		Preface.v
README		README
Records.v		Records.v
Repr.v		Repr.v
Repr.yaml		Repr.yaml
Rich.v		Rich.v
Rules.v		Rules.v
Struct.v		Struct.v
Triples.v		Triples.v
WPgen.v		WPgen.v
WPsem.v		WPsem.v
WPsound.v		WPsound.v
Wand.v		Wand.v
_CoqProject		_CoqProject
flake.lock		flake.lock
flake.nix		flake.nix

Repository files navigation

#########################################################################
                           SOFTWARE FOUNDATIONS
#########################################################################

This directory contains both Rocq scripts (.v files) and more readable
HTML files for the Software Foundations electronic textbook,
covering volume 6, entitled "Separation Logic Foundations".

  - index.html
    The book's cover page and navigation starting point

  - deps.html
    Overview of the ordering of chapters

  - LICENSE
    Explanation of how these files may be redistributed

  - Files SLF*.v
    Contents of the course

  - Files Lib*.v
    Contents of the TLC library

  - Other *.v files
    Implementation of CFML