forked from CertiKOS/rbgs
-
Notifications
You must be signed in to change notification settings - Fork 1
/
_CoqProject
42 lines (40 loc) · 894 Bytes
/
_CoqProject
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
-R coqrel coqrel
-R compcert compcert
-R structures structures
-R lattices lattices
-R models models
-R examples examples
-R compcertox compcertox
-R interfaces interfaces
structures/Poset.v
structures/Lattice.v
structures/Completion.v
structures/Category.v
structures/Monad.v
structures/Effects.v
lattices/Downset.v
lattices/Upset.v
lattices/FCD.v
lattices/LatticeProduct.v
lattices/AdjoinBot.v
models/IntSpec.v
models/Coherence.v
examples/CAL.v
examples/CompCertIntSpec.v
examples/CompCertCAL.v
# examples/ISpecAdjunction.v
examples/RefConv.v
examples/BoundedQueueCode.v
examples/BoundedQueueProof.v
# examples/CompCertSem.v
# CompCertOX formalization
compcertox/Lifting.v
compcertox/AbRel.v
compcertox/CModule.v
compcertox/TensorComp.v
compcertox/SkelLinking.v
compcertox/Composition.v
interfaces/Category.v
interfaces/Functor.v
interfaces/MonoidalCategory.v
interfaces/ConcreteCategory.v