Extracting a Data Flow Analyser in Constructive Logic
You can find here the Coq sources of the development of the article
Extracting a Data Flow Analyser in Constructive Logic.
Here is the list of the differents files used
The main file is last.html.
You can download all .v files and compile them with the given makefile (with Coq 7.4).
Index
| Global Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(34 entries) |
| Lemma Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(13 entries) |
| Constructor Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(6 entries) |
| Inductive Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(2 entries) |
| Definition Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(12 entries) |
| Module Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(1 entry) |
Global Index
A
AbComp [definition, in AbVal]
AbComp_correct [lemma, in AbVal]
AbComp_monotone [lemma, in AbVal]
AbIf_NZ [definition, in AbVal]
AbIf_NZ_monotone [lemma, in AbVal]
AbIf_NZ_prop [lemma, in AbVal]
AbIf_Z [definition, in AbVal]
AbIf_Z_monotone [lemma, in AbVal]
AbIf_Z_prop [lemma, in AbVal]
AbMinus [definition, in AbVal]
AbMinus_correct [lemma, in AbVal]
AbMinus_monotone [lemma, in AbVal]
AbMult [definition, in AbVal]
AbMult_correct [lemma, in AbVal]
AbMult_monotone [lemma, in AbVal]
AbNum [inductive, in AbVal]
AbNumjoin [definition, in AbVal]
AbNumOrder [inductive, in AbVal]
AbPlus [definition, in AbVal]
AbPlus_correct [lemma, in AbVal]
AbPlus_monotone [lemma, in AbVal]
AbVal [module]
acc_property_const [definition, in AbVal]
acc_property_top [definition, in AbVal]
B
betaNum [definition, in AbVal]
bot [constructor, in AbVal]
bot_order [constructor, in AbVal]
C
const [constructor, in AbVal]
const_order [constructor, in AbVal]
L
LatAbNum [definition, in AbVal]
R
R_Num [definition, in AbVal]
R_Num_monotonicity [lemma, in AbVal]
T
top [constructor, in AbVal]
top_order [constructor, in AbVal]
Lemma Index
A
AbComp_correct [in AbVal]
AbComp_monotone [in AbVal]
AbIf_NZ_monotone [in AbVal]
AbIf_NZ_prop [in AbVal]
AbIf_Z_monotone [in AbVal]
AbIf_Z_prop [in AbVal]
AbMinus_correct [in AbVal]
AbMinus_monotone [in AbVal]
AbMult_correct [in AbVal]
AbMult_monotone [in AbVal]
AbPlus_correct [in AbVal]
AbPlus_monotone [in AbVal]
R
R_Num_monotonicity [in AbVal]
Constructor Index
B
bot [in AbVal]
bot_order [in AbVal]
C
const [in AbVal]
const_order [in AbVal]
T
top [in AbVal]
top_order [in AbVal]
Inductive Index
A
AbNum [in AbVal]
AbNumOrder [in AbVal]
Definition Index
A
AbComp [in AbVal]
AbIf_NZ [in AbVal]
AbIf_Z [in AbVal]
AbMinus [in AbVal]
AbMult [in AbVal]
AbNumjoin [in AbVal]
AbPlus [in AbVal]
acc_property_const [in AbVal]
acc_property_top [in AbVal]
B
betaNum [in AbVal]
L
LatAbNum [in AbVal]
R
R_Num [in AbVal]
Module Index
A
AbVal
| Global Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(34 entries) |
| Lemma Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(13 entries) |
| Constructor Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(6 entries) |
| Inductive Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(2 entries) |
| Definition Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(12 entries) |
| Module Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(1 entry) |
This page has been generated by coqdoc