Skip to content

Latest commit

 

History

History
 
 

msl

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
Axioms.v
Axioms.v
 
 
BUILD
BUILD
 
 
CREDITS
CREDITS
 
 
Coqlib2.v
Coqlib2.v
 
 
EXTRACTION
EXTRACTION
 
 
Extensionality.v
Extensionality.v
 
 
README.html
README.html
 
 
SUMMARY
SUMMARY
 
 
age_sepalg.v
age_sepalg.v
 
 
age_to.v
age_to.v
 
 
ageable.v
ageable.v
 
 
alg_seplog.v
alg_seplog.v
 
 
alg_seplog_direct.v
alg_seplog_direct.v
 
 
base.v
base.v
 
 
boolean_alg.v
boolean_alg.v
 
 
cjoins.v
cjoins.v
 
 
combiner_sa.v
combiner_sa.v
 
 
contractive.v
contractive.v
 
 
corable.v
corable.v
 
 
corable_direct.v
corable_direct.v
 
 
corec.v
corec.v
 
 
cross_split.v
cross_split.v
 
 
env.v
env.v
 
 
eq_dec.v
eq_dec.v
 
 
extract.v
extract.v
 
 
functors.v
functors.v
 
 
ghost.v
ghost.v
 
 
ghost_seplog.v
ghost_seplog.v
 
 
iter_sepcon.v
iter_sepcon.v
 
 
join_hom_lemmas.v
join_hom_lemmas.v
 
 
knot.v
knot.v
 
 
knot_full.v
knot_full.v
 
 
knot_full_sa.v
knot_full_sa.v
 
 
knot_full_variant.v
knot_full_variant.v
 
 
knot_hered.v
knot_hered.v
 
 
knot_hered_sa.v
knot_hered_sa.v
 
 
knot_lemmas.v
knot_lemmas.v
 
 
knot_prop.v
knot_prop.v
 
 
knot_setoid.v
knot_setoid.v
 
 
knot_shims.v
knot_shims.v
 
 
knot_unique.v
knot_unique.v
 
 
log_normalize.v
log_normalize.v
 
 
msl_classical.v
msl_classical.v
 
 
msl_direct.v
msl_direct.v
 
 
msl_standard.v
msl_standard.v
 
 
normalize.v
normalize.v
 
 
op_classes.v
op_classes.v
 
 
predicates_hered.v
predicates_hered.v
 
 
predicates_hered_simple.v
predicates_hered_simple.v
 
 
predicates_rec.v
predicates_rec.v
 
 
predicates_sa.v
predicates_sa.v
 
 
predicates_sl.v
predicates_sl.v
 
 
predicates_sl_simple.v
predicates_sl_simple.v
 
 
psepalg.v
psepalg.v
 
 
pshares.v
pshares.v
 
 
ramification_lemmas.v
ramification_lemmas.v
 
 
rmaps.v
rmaps.v
 
 
rmaps_lemmas.v
rmaps_lemmas.v
 
 
sepalg.v
sepalg.v
 
 
sepalg_functors.v
sepalg_functors.v
 
 
sepalg_generators.v
sepalg_generators.v
 
 
sepalg_list.v
sepalg_list.v
 
 
seplog.v
seplog.v
 
 
shares.v
shares.v
 
 
sig_isomorphism.v
sig_isomorphism.v
 
 
simple_CCC.v
simple_CCC.v
 
 
subtypes.v
subtypes.v
 
 
subtypes_sl.v
subtypes_sl.v
 
 
tree_shares.v
tree_shares.v
 
 
wandQ_frame.v
wandQ_frame.v
 
 
wand_frame.v
wand_frame.v
 
 

README.html

<h2>Proof development for Separation Algebras,
Share Accounting, and Indirection Theory
<p>
Andrew W. Appel, Robert Dockins, Aquinas Hobor
<p>
July 2009
<p>
See the SUMMARY file for an explanation.
Note in particular the HOW TO BUILD section.
<p>
LICENSE:  Starting in 2022, MSL is licensed as part of
the Verified Software Toolchain.  The BSD-2-clause
license (for VST) is in the parent directory.
  
</h2>