Skip to content

Latest commit

 

History

History
 
 

sepcomp

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
submit
submit
 
 
submit_shmem
submit_shmem
 
 
Address.v
Address.v
 
 
CompositionalCompiler.v
CompositionalCompiler.v
 
 
CoopCoreSem.v
CoopCoreSem.v
 
 
FiniteMaps.v
FiniteMaps.v
 
 
README
README
 
 
arguments.v
arguments.v
 
 
barebones_simulations.v
barebones_simulations.v
 
 
closed_safety.v
closed_safety.v
 
 
compcert.v
compcert.v
 
 
compiler_correctness.v
compiler_correctness.v
 
 
effect_properties.v
effect_properties.v
 
 
effect_semantics.v
effect_semantics.v
 
 
effect_simulations.v
effect_simulations.v
 
 
effect_simulations_lemmas.v
effect_simulations_lemmas.v
 
 
event_semantics.v
event_semantics.v
 
 
extspec.v
extspec.v
 
 
full_composition.v
full_composition.v
 
 
globalSep.v
globalSep.v
 
 
holes
holes
 
 
internal_diagram_trans.v
internal_diagram_trans.v
 
 
loadpath.v
loadpath.v
 
 
mem_lemmas.v
mem_lemmas.v
 
 
mem_wd.v
mem_wd.v
 
 
nucular_semantics.v
nucular_semantics.v
 
 
reach.v
reach.v
 
 
rg_lemmas.v
rg_lemmas.v
 
 
safety_preservation.v
safety_preservation.v
 
 
semantics.v
semantics.v
 
 
semantics_lemmas.v
semantics_lemmas.v
 
 
simulations.v
simulations.v
 
 
simulations_lemmas.v
simulations_lemmas.v
 
 
sources
sources
 
 
step_lemmas.v
step_lemmas.v
 
 
structured_injections.v
structured_injections.v
 
 
trace_semantics.v
trace_semantics.v
 
 
val_casted.v
val_casted.v
 
 
wholeprog_lemmas.v
wholeprog_lemmas.v
 
 
wholeprog_simulations.v
wholeprog_simulations.v
 
 

README

This directory contains the general separate compilation development
of the VST.

Compositional CompCert (which is one application of the sepcomp
theory) has been moved to vst/compcomp.