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 _ other (1032 entries)
Variable 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 _ other (2 entries)
Library 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 _ other (23 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 _ other (222 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 _ other (494 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 _ other (118 entries)
Projection 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 _ other (15 entries)
Section 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 _ other (28 entries)
Instance 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 _ other (14 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 _ other (109 entries)
Record 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 _ other (7 entries)

Global Index

A

aabort [definition, in langs.L3.semantics]
aaborta [definition, in langs.L3.semantics]
abort [definition, in langs.L3.semantics]
abort [definition, in langs.L2.semantics]
abort [definition, in langs.L2.GCsemantics]
abort [definition, in langs.L1.semantics]
aborta [definition, in langs.L3.semantics]
aborta [definition, in langs.L2.semantics]
aborta [definition, in langs.L2.GCsemantics]
AbortAV [constructor, in langs.L3.semantics]
AbortAV [constructor, in langs.L2.semantics]
AbortAV [constructor, in langs.L2.GCsemantics]
AbortV [constructor, in langs.L3.semantics]
AbortV [constructor, in langs.L2.semantics]
AbortV [constructor, in langs.L2.GCsemantics]
AbortV [constructor, in langs.L1.semantics]
Addr [inductive, in framework.frames]
AddrAV [constructor, in langs.L3.semantics]
AddrAV [constructor, in langs.L2.semantics]
AddrAV [constructor, in langs.L2.GCsemantics]
Addr_ [constructor, in framework.frames]
App [constructor, in langs.L1.syntax]
App [constructor, in langs.L2.syntax]
App [constructor, in langs.L3.syntax]
Asgn [constructor, in langs.L2.syntax]
Asgn [constructor, in langs.L3.syntax]
assign_refs_scopeofFrame [definition, in langs.L3.type_soundness]
assign_refs_ind2 [definition, in langs.L3.semantics]
assign_refs_cons_b2 [constructor, in langs.L3.semantics]
assign_refs_cons_b1 [constructor, in langs.L3.semantics]
assign_refs_b2 [constructor, in langs.L3.semantics]
assign_refs_b1 [constructor, in langs.L3.semantics]
assign_refs_cons [constructor, in langs.L3.semantics]
assign_refs_nil [constructor, in langs.L3.semantics]
assign_refs [inductive, in langs.L3.semantics]
assocData [inductive, in framework.scopes]
assocDataDet [lemma, in framework.scopes]
assocDataofRef [definition, in framework.scopes]
assocDataofRefDet [lemma, in framework.scopes]
assocData_ [constructor, in framework.scopes]
assocScope [inductive, in framework.scopes]
assocScopeDet [lemma, in framework.scopes]
assocScopeofRef [definition, in framework.scopes]
assocScopeofRefDet [lemma, in framework.scopes]
assocScope_ [constructor, in framework.scopes]
AT [definition, in framework.scopes]
AuxV [inductive, in langs.L3.semantics]
AuxV [inductive, in langs.L2.semantics]
AuxV [inductive, in langs.L2.GCsemantics]


B

Binder [constructor, in langs.L2.syntax]
binder [inductive, in langs.L2.syntax]
Binder [constructor, in langs.L3.syntax]
binder [inductive, in langs.L3.syntax]
BoolV [constructor, in langs.L3.semantics]
BoolV [constructor, in langs.L2.semantics]
BoolV [constructor, in langs.L2.GCsemantics]


C

Cdef [constructor, in langs.L3.syntax]
CFalse [constructor, in langs.L2.syntax]
CFalse [constructor, in langs.L3.syntax]
ClosV [constructor, in langs.L3.semantics]
ClosV [constructor, in langs.L2.semantics]
ClosV [constructor, in langs.L2.GCsemantics]
ClosV [constructor, in langs.L1.semantics]
CNum [constructor, in langs.L1.syntax]
CNum [constructor, in langs.L2.syntax]
CNum [constructor, in langs.L3.syntax]
ConstructorV [constructor, in langs.L3.semantics]
CTrue [constructor, in langs.L2.syntax]
CTrue [constructor, in langs.L3.syntax]


D

D [inductive, in framework.scopes]
daunr [constructor, in framework.GC]
ddataofScopeDet [lemma, in framework.scopes]
ddataofScopeP [definition, in framework.scopes]
ddataofScope_scopeofDecl [lemma, in framework.scopes]
Ddec [lemma, in framework.scopes]
De [constructor, in framework.scopes]
decl [inductive, in langs.L2.syntax]
decl [inductive, in langs.L3.syntax]
declofPath [definition, in framework.scopes]
declofRef [inductive, in framework.scopes]
declofRefDet [lemma, in framework.scopes]
declofRef_ [constructor, in framework.scopes]
declsofScopeDet [lemma, in framework.scopes]
declsofScopeP [definition, in framework.scopes]
declsofScope_scopeofDecl [lemma, in framework.scopes]
default [inductive, in langs.L3.type_soundness]
default [inductive, in langs.L2.GCtype_soundness]
default [inductive, in langs.L2.type_soundness]
default [projection, in framework.frames]
defaults [inductive, in framework.frames]
defaults_vtyp' [lemma, in framework.frames]
defaults_vtyp [lemma, in framework.frames]
defaults_nil [constructor, in framework.frames]
DefaultVTyp [record, in framework.frames]
DefaultVTypProperties [section, in framework.frames]
default_vtyp' [lemma, in langs.L3.type_soundness]
default_vtyp' [lemma, in langs.L2.GCtype_soundness]
default_vtyp' [lemma, in langs.L2.type_soundness]
default_cons [constructor, in framework.frames]
default_vtyp [projection, in framework.frames]
DefFunV [constructor, in langs.L3.semantics]
DefFunV [constructor, in langs.L2.semantics]
DefFunV [constructor, in langs.L2.GCsemantics]
def_c [constructor, in langs.L3.type_soundness]
def_r [constructor, in langs.L3.type_soundness]
def_df [constructor, in langs.L3.type_soundness]
def_b [constructor, in langs.L3.type_soundness]
def_n [constructor, in langs.L3.type_soundness]
def_r [constructor, in langs.L2.GCtype_soundness]
def_df [constructor, in langs.L2.GCtype_soundness]
def_b [constructor, in langs.L2.GCtype_soundness]
def_n [constructor, in langs.L2.GCtype_soundness]
def_r [constructor, in langs.L2.type_soundness]
def_df [constructor, in langs.L2.type_soundness]
def_b [constructor, in langs.L2.type_soundness]
def_n [constructor, in langs.L2.type_soundness]
DomEq [definition, in framework.maps]
DomEq_set [lemma, in framework.maps]
Dp [constructor, in framework.scopes]
ds [constructor, in framework.GC]
dunr [constructor, in framework.GC]
dunreach [constructor, in framework.GC]
DVT [instance, in langs.L3.type_soundness]
DVT [instance, in langs.L2.type_soundness]
DVT' [instance, in langs.L2.GCtype_soundness]
DynamicSemantics [section, in langs.L3.semantics]
DynamicSemantics [section, in langs.L2.semantics]
DynamicSemantics [section, in langs.L2.GCsemantics]
DynamicSemantics [section, in langs.L1.semantics]


E

E [constructor, in langs.L1.syntax]
E [constructor, in langs.L2.syntax]
E [constructor, in langs.L3.syntax]
EdgeLabel [inductive, in framework.scopes]
ELdec [lemma, in framework.scopes]
empty [definition, in framework.maps]
emptyHeap [definition, in framework.frames]
emptyHeapNoFrames [lemma, in framework.frames]
Ep [constructor, in framework.scopes]
Error [inductive, in langs.L3.semantics]
Error [inductive, in langs.L2.semantics]
Error [inductive, in langs.L2.GCsemantics]
Error [inductive, in langs.L1.semantics]
eval_objinit_scopeofFrame [definition, in langs.L3.type_soundness]
eval_lhs_scopeofFrame [definition, in langs.L3.type_soundness]
eval_exp_scopeofFrame [definition, in langs.L3.type_soundness]
eval_exp_scopeofFrame_aux [lemma, in langs.L3.type_soundness]
eval_prog_ [constructor, in langs.L3.semantics]
eval_prog [inductive, in langs.L3.semantics]
eval_exp_ind3 [definition, in langs.L3.semantics]
eval_objinit_ind2 [definition, in langs.L3.semantics]
eval_lhs_ind2 [definition, in langs.L3.semantics]
eval_exp_ind2 [definition, in langs.L3.semantics]
eval_objinit_orphan_b2 [constructor, in langs.L3.semantics]
eval_objinit_orphan_b1 [constructor, in langs.L3.semantics]
eval_objinit_orphan [constructor, in langs.L3.semantics]
eval_objinit_b5 [constructor, in langs.L3.semantics]
eval_objinit_b4 [constructor, in langs.L3.semantics]
eval_objinit_b3 [constructor, in langs.L3.semantics]
eval_objinit_b2 [constructor, in langs.L3.semantics]
eval_objinit_b1 [constructor, in langs.L3.semantics]
eval_objinit_null [constructor, in langs.L3.semantics]
eval_objinit_ [constructor, in langs.L3.semantics]
eval_objinit [inductive, in langs.L3.semantics]
eval_lhs_field_b3 [constructor, in langs.L3.semantics]
eval_lhs_field_b2 [constructor, in langs.L3.semantics]
eval_lhs_field_b1 [constructor, in langs.L3.semantics]
eval_lhs_field_null [constructor, in langs.L3.semantics]
eval_lhs_field [constructor, in langs.L3.semantics]
eval_lhs_var_b [constructor, in langs.L3.semantics]
eval_lhs_var_ [constructor, in langs.L3.semantics]
eval_lhs [inductive, in langs.L3.semantics]
eval_new_b1 [constructor, in langs.L3.semantics]
eval_new_ [constructor, in langs.L3.semantics]
eval_seq_b1 [constructor, in langs.L3.semantics]
eval_seq_ [constructor, in langs.L3.semantics]
eval_if_b1 [constructor, in langs.L3.semantics]
eval_if_f [constructor, in langs.L3.semantics]
eval_if_t [constructor, in langs.L3.semantics]
eval_asgn_b3 [constructor, in langs.L3.semantics]
eval_asgn_b2 [constructor, in langs.L3.semantics]
eval_asgn_b1 [constructor, in langs.L3.semantics]
eval_asgn_ [constructor, in langs.L3.semantics]
eval_letrec_b1 [constructor, in langs.L3.semantics]
eval_letrec_ [constructor, in langs.L3.semantics]
eval_letseq_b1 [constructor, in langs.L3.semantics]
eval_letseq_ [constructor, in langs.L3.semantics]
eval_letpar_b1 [constructor, in langs.L3.semantics]
eval_letpar_ [constructor, in langs.L3.semantics]
eval_app_b2 [constructor, in langs.L3.semantics]
eval_app_b1 [constructor, in langs.L3.semantics]
eval_app_dfun [constructor, in langs.L3.semantics]
eval_app [constructor, in langs.L3.semantics]
eval_fn_ [constructor, in langs.L3.semantics]
eval_lhs_b2 [constructor, in langs.L3.semantics]
eval_lhs_b1 [constructor, in langs.L3.semantics]
eval_lhs_ [constructor, in langs.L3.semantics]
eval_gt_b2 [constructor, in langs.L3.semantics]
eval_gt_b1 [constructor, in langs.L3.semantics]
eval_gt_ [constructor, in langs.L3.semantics]
eval_plus_b2 [constructor, in langs.L3.semantics]
eval_plus_b1 [constructor, in langs.L3.semantics]
eval_plus_ [constructor, in langs.L3.semantics]
eval_false_ [constructor, in langs.L3.semantics]
eval_true_ [constructor, in langs.L3.semantics]
eval_cnum_ [constructor, in langs.L3.semantics]
eval_exp [inductive, in langs.L3.semantics]
eval_exp_scopeofFrame [lemma, in langs.L1.type_soundness]
eval_lhs_scopeofFrame [definition, in langs.L2.GCtype_soundness]
eval_exp_scopeofFrame [definition, in langs.L2.GCtype_soundness]
eval_exp_scopeofFrame_aux [lemma, in langs.L2.GCtype_soundness]
eval_prog_ [constructor, in langs.L2.semantics]
eval_prog [inductive, in langs.L2.semantics]
eval_exp_ind3 [definition, in langs.L2.semantics]
eval_lhs_ind2 [definition, in langs.L2.semantics]
eval_exp_ind2 [definition, in langs.L2.semantics]
eval_lhs_field_b2 [constructor, in langs.L2.semantics]
eval_lhs_field_b1 [constructor, in langs.L2.semantics]
eval_lhs_field_null [constructor, in langs.L2.semantics]
eval_lhs_field [constructor, in langs.L2.semantics]
eval_lhs_var_b [constructor, in langs.L2.semantics]
eval_lhs_var_ [constructor, in langs.L2.semantics]
eval_lhs [inductive, in langs.L2.semantics]
eval_new_b1 [constructor, in langs.L2.semantics]
eval_new_ [constructor, in langs.L2.semantics]
eval_seq_b1 [constructor, in langs.L2.semantics]
eval_seq_ [constructor, in langs.L2.semantics]
eval_if_b1 [constructor, in langs.L2.semantics]
eval_if_f [constructor, in langs.L2.semantics]
eval_if_t [constructor, in langs.L2.semantics]
eval_asgn_b3 [constructor, in langs.L2.semantics]
eval_asgn_b2 [constructor, in langs.L2.semantics]
eval_asgn_b1 [constructor, in langs.L2.semantics]
eval_asgn_ [constructor, in langs.L2.semantics]
eval_letrec_b1 [constructor, in langs.L2.semantics]
eval_letrec_ [constructor, in langs.L2.semantics]
eval_letseq_b1 [constructor, in langs.L2.semantics]
eval_letseq_ [constructor, in langs.L2.semantics]
eval_letpar_b1 [constructor, in langs.L2.semantics]
eval_letpar_ [constructor, in langs.L2.semantics]
eval_app_b2 [constructor, in langs.L2.semantics]
eval_app_b1 [constructor, in langs.L2.semantics]
eval_app_dfun [constructor, in langs.L2.semantics]
eval_app [constructor, in langs.L2.semantics]
eval_fn_ [constructor, in langs.L2.semantics]
eval_lhs_b2 [constructor, in langs.L2.semantics]
eval_lhs_b1 [constructor, in langs.L2.semantics]
eval_lhs_ [constructor, in langs.L2.semantics]
eval_gt_b2 [constructor, in langs.L2.semantics]
eval_gt_b1 [constructor, in langs.L2.semantics]
eval_gt_ [constructor, in langs.L2.semantics]
eval_plus_b2 [constructor, in langs.L2.semantics]
eval_plus_b1 [constructor, in langs.L2.semantics]
eval_plus_ [constructor, in langs.L2.semantics]
eval_false_ [constructor, in langs.L2.semantics]
eval_true_ [constructor, in langs.L2.semantics]
eval_cnum_ [constructor, in langs.L2.semantics]
eval_exp [inductive, in langs.L2.semantics]
eval_lhs_scopeofFrame [definition, in langs.L2.type_soundness]
eval_exp_scopeofFrame [definition, in langs.L2.type_soundness]
eval_exp_scopeofFrame_aux [lemma, in langs.L2.type_soundness]
eval_prog_ [constructor, in langs.L2.GCsemantics]
eval_prog [inductive, in langs.L2.GCsemantics]
eval_exp_ind3 [definition, in langs.L2.GCsemantics]
eval_lhs_ind2 [definition, in langs.L2.GCsemantics]
eval_exp_ind2 [definition, in langs.L2.GCsemantics]
eval_lhs_field_b2 [constructor, in langs.L2.GCsemantics]
eval_lhs_field_b1 [constructor, in langs.L2.GCsemantics]
eval_lhs_field_null [constructor, in langs.L2.GCsemantics]
eval_lhs_field [constructor, in langs.L2.GCsemantics]
eval_lhs_var_b [constructor, in langs.L2.GCsemantics]
eval_lhs_var_ [constructor, in langs.L2.GCsemantics]
eval_lhs [inductive, in langs.L2.GCsemantics]
eval_new_b1 [constructor, in langs.L2.GCsemantics]
eval_new_ [constructor, in langs.L2.GCsemantics]
eval_seq_b1 [constructor, in langs.L2.GCsemantics]
eval_seq_ [constructor, in langs.L2.GCsemantics]
eval_if_b1 [constructor, in langs.L2.GCsemantics]
eval_if_f [constructor, in langs.L2.GCsemantics]
eval_if_t [constructor, in langs.L2.GCsemantics]
eval_asgn_b3 [constructor, in langs.L2.GCsemantics]
eval_asgn_b2 [constructor, in langs.L2.GCsemantics]
eval_asgn_b1 [constructor, in langs.L2.GCsemantics]
eval_asgn_ [constructor, in langs.L2.GCsemantics]
eval_letrec_b1 [constructor, in langs.L2.GCsemantics]
eval_letrec_ [constructor, in langs.L2.GCsemantics]
eval_letseq_b1 [constructor, in langs.L2.GCsemantics]
eval_letseq_ [constructor, in langs.L2.GCsemantics]
eval_letpar_b1 [constructor, in langs.L2.GCsemantics]
eval_letpar_ [constructor, in langs.L2.GCsemantics]
eval_app_b2 [constructor, in langs.L2.GCsemantics]
eval_app_b1 [constructor, in langs.L2.GCsemantics]
eval_app_dfun [constructor, in langs.L2.GCsemantics]
eval_app [constructor, in langs.L2.GCsemantics]
eval_fn_ [constructor, in langs.L2.GCsemantics]
eval_lhs_b2 [constructor, in langs.L2.GCsemantics]
eval_lhs_b1 [constructor, in langs.L2.GCsemantics]
eval_lhs_ [constructor, in langs.L2.GCsemantics]
eval_gt_b2 [constructor, in langs.L2.GCsemantics]
eval_gt_b1 [constructor, in langs.L2.GCsemantics]
eval_gt_ [constructor, in langs.L2.GCsemantics]
eval_plus_b2 [constructor, in langs.L2.GCsemantics]
eval_plus_b1 [constructor, in langs.L2.GCsemantics]
eval_plus_ [constructor, in langs.L2.GCsemantics]
eval_false_ [constructor, in langs.L2.GCsemantics]
eval_true_ [constructor, in langs.L2.GCsemantics]
eval_cnum_ [constructor, in langs.L2.GCsemantics]
eval_gc_ [constructor, in langs.L2.GCsemantics]
eval_exp [inductive, in langs.L2.GCsemantics]
eval_prog_ [constructor, in langs.L1.semantics]
eval_prog [inductive, in langs.L1.semantics]
eval_app_b2 [constructor, in langs.L1.semantics]
eval_app_b1 [constructor, in langs.L1.semantics]
eval_app [constructor, in langs.L1.semantics]
eval_fn_ [constructor, in langs.L1.semantics]
eval_var_b2 [constructor, in langs.L1.semantics]
eval_var_b1 [constructor, in langs.L1.semantics]
eval_var_ [constructor, in langs.L1.semantics]
eval_plus_b2 [constructor, in langs.L1.semantics]
eval_plus_b1 [constructor, in langs.L1.semantics]
eval_plus_ [constructor, in langs.L1.semantics]
eval_cnum_ [constructor, in langs.L1.semantics]
eval_exp [inductive, in langs.L1.semantics]
exp [inductive, in langs.L1.syntax]
exp [inductive, in langs.L2.syntax]
exp [inductive, in langs.L3.syntax]
expScope [definition, in langs.L1.syntax]
expScope [definition, in langs.L2.syntax]
expScope [definition, in langs.L3.syntax]
expType [definition, in langs.L1.syntax]
expType [definition, in langs.L2.syntax]
expType [definition, in langs.L3.syntax]
exp_preservation [lemma, in langs.L3.type_soundness]
exp_preservation [lemma, in langs.L1.type_soundness]
exp_preservation [lemma, in langs.L2.GCtype_soundness]
exp_preservation [lemma, in langs.L2.type_soundness]


F

FH [instance, in langs.L3.type_soundness]
FH [instance, in langs.L2.GCtype_soundness]
FH [instance, in langs.L2.type_soundness]
FH [instance, in langs.L1.semantics]
Field [constructor, in langs.L2.syntax]
Field [constructor, in langs.L3.syntax]
fillFrame [definition, in framework.frames]
fillFrameDiff [lemma, in framework.frames]
fillFrameDiff' [lemma, in framework.frames]
fillFrameFrames [lemma, in framework.frames]
fillFrameSame [lemma, in framework.frames]
fillFrameSame' [lemma, in framework.frames]
fillFrameSlotDiff [lemma, in framework.frames]
fillFrameSlotDiff' [lemma, in framework.frames]
fillFrame_vtyp' [lemma, in langs.L3.type_soundness]
fillFrame_vtyp' [lemma, in langs.L1.type_soundness]
fillFrame_vtyp' [lemma, in langs.L2.GCtype_soundness]
fillFrame_vtyp' [lemma, in langs.L2.type_soundness]
fillFrame_vtyp [projection, in framework.frames]
fill_rec_scopeofFrame [definition, in langs.L3.type_soundness]
fill_seq_scopeofFrame [definition, in langs.L3.type_soundness]
fill_par_scopeofFrame [definition, in langs.L3.type_soundness]
fill_rec_ind2 [definition, in langs.L3.semantics]
fill_seq_ind2 [definition, in langs.L3.semantics]
fill_par_ind2 [definition, in langs.L3.semantics]
fill_rec_cons_b2 [constructor, in langs.L3.semantics]
fill_rec_cons_b1 [constructor, in langs.L3.semantics]
fill_rec_cons [constructor, in langs.L3.semantics]
fill_rec_b2 [constructor, in langs.L3.semantics]
fill_rec_b1 [constructor, in langs.L3.semantics]
fill_rec_nil [constructor, in langs.L3.semantics]
fill_slots_rec [inductive, in langs.L3.semantics]
fill_seq_cons_b2 [constructor, in langs.L3.semantics]
fill_seq_cons_b1 [constructor, in langs.L3.semantics]
fill_seq_cons [constructor, in langs.L3.semantics]
fill_seq_b2 [constructor, in langs.L3.semantics]
fill_seq_b1 [constructor, in langs.L3.semantics]
fill_seq_nil [constructor, in langs.L3.semantics]
fill_slots_seq [inductive, in langs.L3.semantics]
fill_par_cons_b2 [constructor, in langs.L3.semantics]
fill_par_cons_b1 [constructor, in langs.L3.semantics]
fill_par_cons [constructor, in langs.L3.semantics]
fill_par_b2 [constructor, in langs.L3.semantics]
fill_par_b1 [constructor, in langs.L3.semantics]
fill_par_nil [constructor, in langs.L3.semantics]
fill_slots_par [inductive, in langs.L3.semantics]
fill_rec_scopeofFrame [definition, in langs.L2.GCtype_soundness]
fill_seq_scopeofFrame [definition, in langs.L2.GCtype_soundness]
fill_par_scopeofFrame [definition, in langs.L2.GCtype_soundness]
fill_rec_ind2 [definition, in langs.L2.semantics]
fill_seq_ind2 [definition, in langs.L2.semantics]
fill_par_ind2 [definition, in langs.L2.semantics]
fill_rec_cons_b2 [constructor, in langs.L2.semantics]
fill_rec_cons_b1 [constructor, in langs.L2.semantics]
fill_rec_cons [constructor, in langs.L2.semantics]
fill_rec_b2 [constructor, in langs.L2.semantics]
fill_rec_b1 [constructor, in langs.L2.semantics]
fill_rec_nil [constructor, in langs.L2.semantics]
fill_slots_rec [inductive, in langs.L2.semantics]
fill_seq_cons_b2 [constructor, in langs.L2.semantics]
fill_seq_cons_b1 [constructor, in langs.L2.semantics]
fill_seq_cons [constructor, in langs.L2.semantics]
fill_seq_b2 [constructor, in langs.L2.semantics]
fill_seq_b1 [constructor, in langs.L2.semantics]
fill_seq_nil [constructor, in langs.L2.semantics]
fill_slots_seq [inductive, in langs.L2.semantics]
fill_par_cons_b2 [constructor, in langs.L2.semantics]
fill_par_cons_b1 [constructor, in langs.L2.semantics]
fill_par_cons [constructor, in langs.L2.semantics]
fill_par_b2 [constructor, in langs.L2.semantics]
fill_par_b1 [constructor, in langs.L2.semantics]
fill_par_nil [constructor, in langs.L2.semantics]
fill_slots_par [inductive, in langs.L2.semantics]
fill_rec_scopeofFrame [definition, in langs.L2.type_soundness]
fill_seq_scopeofFrame [definition, in langs.L2.type_soundness]
fill_par_scopeofFrame [definition, in langs.L2.type_soundness]
fill_rec_ind2 [definition, in langs.L2.GCsemantics]
fill_seq_ind2 [definition, in langs.L2.GCsemantics]
fill_par_ind2 [definition, in langs.L2.GCsemantics]
fill_rec_cons_b2 [constructor, in langs.L2.GCsemantics]
fill_rec_cons_b1 [constructor, in langs.L2.GCsemantics]
fill_rec_cons [constructor, in langs.L2.GCsemantics]
fill_rec_b2 [constructor, in langs.L2.GCsemantics]
fill_rec_b1 [constructor, in langs.L2.GCsemantics]
fill_rec_nil [constructor, in langs.L2.GCsemantics]
fill_slots_rec [inductive, in langs.L2.GCsemantics]
fill_seq_cons_b2 [constructor, in langs.L2.GCsemantics]
fill_seq_cons_b1 [constructor, in langs.L2.GCsemantics]
fill_seq_cons [constructor, in langs.L2.GCsemantics]
fill_seq_b2 [constructor, in langs.L2.GCsemantics]
fill_seq_b1 [constructor, in langs.L2.GCsemantics]
fill_seq_nil [constructor, in langs.L2.GCsemantics]
fill_slots_seq [inductive, in langs.L2.GCsemantics]
fill_par_cons_b2 [constructor, in langs.L2.GCsemantics]
fill_par_cons_b1 [constructor, in langs.L2.GCsemantics]
fill_par_cons [constructor, in langs.L2.GCsemantics]
fill_par_b2 [constructor, in langs.L2.GCsemantics]
fill_par_b1 [constructor, in langs.L2.GCsemantics]
fill_par_nil [constructor, in langs.L2.GCsemantics]
fill_slots_par [inductive, in langs.L2.GCsemantics]
fldDecl [definition, in langs.L2.syntax]
Flddecl [constructor, in langs.L2.syntax]
FldDecl [constructor, in langs.L3.syntax]
fldDT [definition, in langs.L3.syntax]
fldI [definition, in langs.L3.syntax]
fldType [definition, in langs.L2.syntax]
fld_decl [inductive, in langs.L2.syntax]
fld_decl [inductive, in langs.L3.syntax]
Fn [constructor, in langs.L1.syntax]
Fn [constructor, in langs.L2.syntax]
Fn [constructor, in langs.L3.syntax]
ForallFold2 [inductive, in framework.prop_fold]
ForallFold2_cons [constructor, in framework.prop_fold]
ForallFold2_nil [constructor, in framework.prop_fold]
forall2_in [lemma, in langs.L3.type_soundness]
forall2_sub_trans [lemma, in langs.L3.type_soundness]
frame [definition, in framework.frames]
FrameAV [constructor, in langs.L3.semantics]
FrameAV [constructor, in langs.L2.semantics]
FrameAV [constructor, in langs.L2.GCsemantics]
FrameHeap [record, in framework.frames]
FrameHeapProperties [section, in framework.frames]
FrameHeapProperties.CombiningStaticAndDynamic [section, in framework.frames]
FrameId [definition, in framework.frames]
FrameIdDec [lemma, in framework.frames]
frames [library]
frefers [inductive, in framework.GC]
fr_slot [constructor, in framework.GC]
fr_link [constructor, in framework.GC]


G

g [projection, in framework.scopes]
GC [library]
GCsemantics [library]
GCtype_soundness [library]
get [definition, in framework.maps]
getAddr [inductive, in framework.frames]
getAddrDet [lemma, in framework.frames]
getAddr_ [constructor, in framework.frames]
getAddr_good_frame_sub [lemma, in framework.sub]
getAddr_typofDecl_getSlot_sub [lemma, in framework.sub]
getAddr_getSlot_sub [lemma, in framework.sub]
getAddr_in_ds_sub [lemma, in framework.sub]
getAddr_scopeofFrame_sub [lemma, in framework.sub]
getRef [inductive, in framework.frames]
getRefDet [lemma, in framework.frames]
getRef_ [constructor, in framework.frames]
getSlot [inductive, in framework.frames]
getSlotDet [lemma, in framework.frames]
getSlotFrame [lemma, in framework.frames]
getSlots_ [constructor, in framework.frames]
getSlot_ [constructor, in framework.frames]
get_empty [lemma, in framework.maps]
get_set_other [lemma, in framework.maps]
get_set_same [lemma, in framework.maps]
get_remove_other [lemma, in framework.maps]
get_remove_same [lemma, in framework.maps]
good [definition, in langs.L3.semantics]
good [definition, in langs.L2.semantics]
good [definition, in langs.L2.GCsemantics]
good [definition, in langs.L1.semantics]
Goodness [section, in framework.frames]
good_roots_decomp [lemma, in langs.L2.GCtype_soundness]
good_roots_drop2 [lemma, in langs.L2.GCtype_soundness]
good_roots_drop [lemma, in langs.L2.GCtype_soundness]
good_roots_swap [lemma, in langs.L2.GCtype_soundness]
good_roots [definition, in langs.L2.GCtype_soundness]
good_frame_setSlot [lemma, in framework.frames]
good_frame_getSlot [lemma, in framework.frames]
good_addr [lemma, in framework.frames]
good_path [lemma, in framework.frames]
good_path0 [lemma, in framework.frames]
good_heap [definition, in framework.frames]
good_frame [definition, in framework.frames]
good_frame_getSlot_sub [lemma, in framework.sub]
good_frame_setSlot_sub [lemma, in framework.sub]
good_addr_sub [lemma, in framework.sub]
good_path_sub [lemma, in framework.sub]
good_heap2good_sub_heap [lemma, in framework.sub]
good_frame2good_sub_frame [lemma, in framework.sub]
good_sub_heap [definition, in framework.sub]
good_sub_frame [definition, in framework.sub]
good_heap_removeUnreachable [lemma, in framework.GC]
good_heap_removeAllUnreferenced [lemma, in framework.GC]
good_heap_removeUnreferenced [lemma, in framework.GC]
good_heap_safeRemoval [lemma, in framework.GC]
Graph [record, in framework.scopes]
Gt [constructor, in langs.L2.syntax]
Gt [constructor, in langs.L3.syntax]


I

I [constructor, in framework.scopes]
ident [definition, in framework.scopes]
If [constructor, in langs.L2.syntax]
If [constructor, in langs.L3.syntax]
initDefault [inductive, in framework.frames]
initDefaultDiff_scopeofFrame [lemma, in framework.frames]
initDefaultFrames [lemma, in framework.frames]
initDefaultSame_scopeofFrame [lemma, in framework.frames]
initDefault_good_roots [lemma, in langs.L2.GCtype_soundness]
initDefault_good_heap1 [lemma, in framework.frames]
initDefault_good_heap0 [lemma, in framework.frames]
initDefault_good_heap [lemma, in framework.frames]
initDefault_good_frame [lemma, in framework.frames]
initDefault_vtyp [lemma, in framework.frames]
initDefault_ [constructor, in framework.frames]
initDefault_good_heap2_sub [lemma, in framework.sub]
initDefault_good_heap0_sub [lemma, in framework.sub]
initDefault_good_heap1_sub [lemma, in framework.sub]
initDefault_good_heap_sub [lemma, in framework.sub]
initDefault_good_frame_sub [lemma, in framework.sub]
initExp [definition, in langs.L3.syntax]
initFrame [inductive, in framework.frames]
initFrameDiff [lemma, in framework.frames]
initFrameDiff_scopeofFrame [lemma, in framework.frames]
initFrameDiff' [lemma, in framework.frames]
initFrameFrames [lemma, in framework.frames]
initFrameSame [lemma, in framework.frames]
initFrameSame_scopeofFrame [lemma, in framework.frames]
initFrameSlotDiff' [lemma, in framework.frames]
initFrame_good_heap2 [lemma, in framework.frames]
initFrame_good_heap1 [lemma, in framework.frames]
initFrame_good_heap0 [lemma, in framework.frames]
initFrame_good_heap [lemma, in framework.frames]
initFrame_good_frame [lemma, in framework.frames]
initFrame_well_typed [lemma, in framework.frames]
initFrame_well_bound2 [lemma, in framework.frames]
initFrame_well_bound1 [lemma, in framework.frames]
initFrame_well_bound [lemma, in framework.frames]
initFrame_other_good_frame [lemma, in framework.frames]
initFrame_other_well_typed [lemma, in framework.frames]
initFrame_other_well_bound [lemma, in framework.frames]
initFrame_vtyp [lemma, in framework.frames]
initFrame_ [constructor, in framework.frames]
initFrame_good_heap_sub [lemma, in framework.sub]
initFrame_other_good_frame_sub [lemma, in framework.sub]
initFrame_other_well_typed_sub [lemma, in framework.sub]
initFrame_good_frame_sub [lemma, in framework.sub]
initFrame_well_typed_sub [lemma, in framework.sub]
Initializer [constructor, in langs.L3.syntax]
initializer [inductive, in langs.L3.syntax]
initRef [definition, in langs.L3.syntax]
init_decls_sound [lemma, in langs.L3.type_soundness]
init_decl_nil [constructor, in langs.L3.semantics]
init_decl_rdef [constructor, in langs.L3.semantics]
init_decls [inductive, in langs.L3.semantics]
in_2 [lemma, in langs.L3.type_soundness]
in_2 [lemma, in langs.L2.GCtype_soundness]
in_2 [lemma, in langs.L2.type_soundness]
in_keys_remove [lemma, in framework.maps]
in_keys_set [lemma, in framework.maps]
in_values [lemma, in framework.maps]
in_keys [lemma, in framework.maps]
is_val [definition, in langs.L2.syntax]
is_val [definition, in langs.L3.syntax]


K

keys [definition, in framework.maps]
keys_in [lemma, in framework.maps]


L

LetPar [constructor, in langs.L2.syntax]
LetPar [constructor, in langs.L3.syntax]
LetRec [constructor, in langs.L2.syntax]
LetRec [constructor, in langs.L3.syntax]
LetSeq [constructor, in langs.L2.syntax]
LetSeq [constructor, in langs.L3.syntax]
lhs [inductive, in langs.L2.syntax]
Lhs [constructor, in langs.L2.syntax]
lhs [inductive, in langs.L3.syntax]
Lhs [constructor, in langs.L3.syntax]
linksofFrame [inductive, in framework.frames]
linksofFrameDet [lemma, in framework.frames]
linksofFrame_ [constructor, in framework.frames]
linksofScopeDet [lemma, in framework.scopes]
linksofScopeP [definition, in framework.scopes]
llinksofFrame [inductive, in framework.frames]
llinksofFrameDet [lemma, in framework.frames]
llinksofFrame_ [constructor, in framework.frames]
llinksofScopeDet [lemma, in framework.scopes]
llinksofScopeP [definition, in framework.scopes]
lookup [inductive, in framework.frames]
lookupD [constructor, in framework.frames]
lookupDet [lemma, in framework.frames]
lookupI [constructor, in framework.frames]
LookupPredicates [section, in framework.scopes]


M

map [definition, in framework.maps]
MapDomains [section, in framework.maps]
MapDomains.DecEq [variable, in framework.maps]
Maps [section, in framework.maps]
maps [library]
Maps.Kdec [variable, in framework.maps]


N

New [constructor, in langs.L2.syntax]
New [constructor, in langs.L3.syntax]
newFrame [definition, in framework.frames]
newFrameDiff [lemma, in framework.frames]
newFrameDiff' [lemma, in framework.frames]
newFrameFrames [lemma, in framework.frames]
newFrameNew [lemma, in framework.frames]
newFrameSame [lemma, in framework.frames]
newFrameSlotDiff [lemma, in framework.frames]
newFrameSlotDiff' [lemma, in framework.frames]
newFrameSlotSame [lemma, in framework.frames]
newFrame_vtyp' [lemma, in langs.L3.type_soundness]
newFrame_vtyp' [lemma, in langs.L1.type_soundness]
newFrame_vtyp' [lemma, in langs.L2.GCtype_soundness]
newFrame_vtyp' [lemma, in langs.L2.type_soundness]
newFrame_vtyp [projection, in framework.frames]
not_keys_in [lemma, in framework.maps]
not_in_keys [lemma, in framework.maps]
NullPointer [constructor, in langs.L3.semantics]
NullPointer [constructor, in langs.L2.semantics]
NullPointer [constructor, in langs.L2.GCsemantics]
NullV [constructor, in langs.L3.semantics]
NullV [constructor, in langs.L2.semantics]
NullV [constructor, in langs.L2.GCsemantics]
NumV [constructor, in langs.L3.semantics]
NumV [constructor, in langs.L2.semantics]
NumV [constructor, in langs.L2.GCsemantics]
NumV [constructor, in langs.L1.semantics]


O

ObjectV [constructor, in langs.L3.semantics]


P

P [constructor, in framework.scopes]
path [inductive, in framework.scopes]
pathofRefDet [lemma, in framework.scopes]
pathofRefP [definition, in framework.scopes]
path_connectivity' [lemma, in framework.scopes]
path_connectivity [projection, in framework.scopes]
Plus [constructor, in langs.L1.syntax]
Plus [constructor, in langs.L2.syntax]
Plus [constructor, in langs.L3.syntax]
PredicateForms [section, in framework.scopes]
pre_exp [inductive, in langs.L1.syntax]
pre_exp [inductive, in langs.L2.syntax]
pre_exp [inductive, in langs.L3.syntax]
Prog [constructor, in langs.L1.syntax]
prog [inductive, in langs.L1.syntax]
Prog [constructor, in langs.L2.syntax]
prog [inductive, in langs.L2.syntax]
Prog [constructor, in langs.L3.syntax]
prog [inductive, in langs.L3.syntax]
prog_sound [lemma, in langs.L3.type_soundness]
prog_sound [lemma, in langs.L1.type_soundness]
prog_sound [lemma, in langs.L2.GCtype_soundness]
prog_sound [lemma, in langs.L2.type_soundness]
prop_fold [library]


R

R [inductive, in framework.scopes]
Rdec [lemma, in framework.scopes]
Rdef [constructor, in langs.L2.syntax]
Re [constructor, in framework.scopes]
reachable [inductive, in framework.GC]
RecordV [constructor, in langs.L2.semantics]
RecordV [constructor, in langs.L2.GCsemantics]
refsofScopeDet [lemma, in framework.scopes]
refsofScopeP [definition, in framework.scopes]
remove [definition, in framework.maps]
removeAllUnreachable [inductive, in framework.GC]
removeAllUnreachable_safe [lemma, in framework.GC]
removeAllUnreferenced [inductive, in framework.GC]
removeAllUnreferenced_safe [lemma, in framework.GC]
removeFrame [definition, in framework.frames]
removeFrameFrames [lemma, in framework.frames]
removeFrameFrames' [lemma, in framework.frames]
removeFrameFrames0 [lemma, in framework.frames]
removeFrames [inductive, in framework.frames]
removeFrameSame [lemma, in framework.frames]
removeFrameScope [lemma, in framework.frames]
removeFramesFrames [lemma, in framework.frames]
removeFrameSlot [lemma, in framework.frames]
removeFramesSame [lemma, in framework.frames]
removeFramesScope [lemma, in framework.frames]
removeFramesSlot [lemma, in framework.frames]
removeFrames_good_roots [lemma, in langs.L2.GCtype_soundness]
removeFrames_vtyp [lemma, in langs.L2.GCtype_soundness]
removeFrames_vtyp [projection, in framework.GC]
removeFrames_frefers [lemma, in framework.GC]
removeFrame_good_roots [lemma, in langs.L2.GCtype_soundness]
removeFrame_frefers [lemma, in framework.GC]
removeUnreferenced [inductive, in framework.GC]
removeUnreferenced_safe [lemma, in framework.GC]
remove_in_keys [lemma, in framework.maps]
re_fref [constructor, in framework.GC]
re_refl [constructor, in framework.GC]
rfs_cons [constructor, in framework.frames]
rfs_nil [constructor, in framework.frames]
RGATProperties [section, in framework.scopes]
rlookup [definition, in framework.scopes]
rlookupDet [lemma, in framework.scopes]


S

safeRemoval [inductive, in framework.GC]
SanityChecks [section, in framework.scopes]
ScopeId [definition, in framework.scopes]
ScopeIdDec [lemma, in framework.scopes]
scopeofDeclDet [lemma, in framework.scopes]
scopeofDeclP [definition, in framework.scopes]
scopeofDecl_sanity2 [lemma, in framework.scopes]
scopeofDecl_sanity1 [lemma, in framework.scopes]
scopeofFrame [inductive, in framework.frames]
scopeofFrameDet [lemma, in framework.frames]
scopeofFrameFrame [lemma, in framework.frames]
scopeofFrame_ [constructor, in framework.frames]
scopeofRefDet [lemma, in framework.scopes]
scopeofRefP [definition, in framework.scopes]
scopeofRef_sanity2 [lemma, in framework.scopes]
scopeofRef_sanity1 [lemma, in framework.scopes]
scopes [library]
semantics [library]
semantics [library]
semantics [library]
Seq [constructor, in langs.L2.syntax]
Seq [constructor, in langs.L3.syntax]
set [definition, in framework.maps]
setSlot [inductive, in framework.frames]
setSlotFrame [lemma, in framework.frames]
setSlotFrames [lemma, in framework.frames]
setSlotSame [lemma, in framework.frames]
setSlotScope [lemma, in framework.frames]
setSlotSlotDiff [lemma, in framework.frames]
setSlotSlotDiff' [lemma, in framework.frames]
setSlotSlotSame [lemma, in framework.frames]
setSlot_vtyp' [lemma, in langs.L3.type_soundness]
setSlot_vtyp' [lemma, in langs.L1.type_soundness]
setSlot_good_roots [lemma, in langs.L2.GCtype_soundness]
setSlot_vtyp' [lemma, in langs.L2.GCtype_soundness]
setSlot_vtyp' [lemma, in langs.L2.type_soundness]
setSlot_good_heap [lemma, in framework.frames]
setSlot_other_good_frame [lemma, in framework.frames]
setSlot_other_well_typed [lemma, in framework.frames]
setSlot_other_well_bound [lemma, in framework.frames]
setSlot_good_frame [lemma, in framework.frames]
setSlot_well_typed [lemma, in framework.frames]
setSlot_well_bound [lemma, in framework.frames]
setSlot_vtyp [projection, in framework.frames]
setSlot_ [constructor, in framework.frames]
setSlot_good_heap_sub [lemma, in framework.sub]
setSlot_good_sub_frame [lemma, in framework.sub]
setSlot_other_good_sub_frame [lemma, in framework.sub]
setSlot_other_well_sub_typed [lemma, in framework.sub]
setSlot_well_typed_sub [lemma, in framework.sub]
set_in_keys [lemma, in framework.maps]
slookupDet [lemma, in framework.scopes]
slookup_ddata [lemma, in framework.scopes]
slookup_declofPath [lemma, in framework.scopes]
slotsofFrame [inductive, in framework.frames]
slotsofFrameDet [lemma, in framework.frames]
split_b [definition, in langs.L2.syntax]
split_f [definition, in langs.L3.syntax]
split_i [definition, in langs.L3.syntax]
split_b [definition, in langs.L3.syntax]
ST [instance, in langs.L3.type_soundness]
sub [projection, in framework.sub]
sub [library]
SubTyping [record, in framework.sub]
sub_class_upcast [lemma, in langs.L3.type_soundness]
sub_tclassdef [lemma, in langs.L3.type_soundness]
sub_tclass [lemma, in langs.L3.type_soundness]
sub_tarrow [lemma, in langs.L3.type_soundness]
sub_bool [lemma, in langs.L3.type_soundness]
sub_int [lemma, in langs.L3.type_soundness]
sub_fun [constructor, in langs.L3.well_typedness]
sub_rec [constructor, in langs.L3.well_typedness]
sub_trans [projection, in framework.sub]
sub_refl [projection, in framework.sub]
sub' [inductive, in langs.L3.well_typedness]
sub'_refl [lemma, in langs.L3.type_soundness]
sub'_trans [lemma, in langs.L3.type_soundness]
sub'_trans [constructor, in langs.L3.well_typedness]
sub'_refl [constructor, in langs.L3.well_typedness]
sub1 [inductive, in langs.L3.well_typedness]
syntax [library]
syntax [library]
syntax [library]


T

T [inductive, in langs.L1.syntax]
T [inductive, in langs.L2.syntax]
T [inductive, in langs.L3.syntax]
Tarrow [constructor, in langs.L1.syntax]
Tarrow [constructor, in langs.L2.syntax]
Tarrow [constructor, in langs.L3.syntax]
Tbool [constructor, in langs.L2.syntax]
Tbool [constructor, in langs.L3.syntax]
Tclass [constructor, in langs.L3.syntax]
TclassDef [constructor, in langs.L3.syntax]
Tint [constructor, in langs.L1.syntax]
Tint [constructor, in langs.L2.syntax]
Tint [constructor, in langs.L3.syntax]
Trecord [constructor, in langs.L2.syntax]
TV [section, in framework.sub]
TypeSoundness [section, in langs.L3.type_soundness]
TypeSoundness [section, in langs.L1.type_soundness]
TypeSoundness [section, in langs.L2.GCtype_soundness]
TypeSoundness [section, in langs.L2.type_soundness]
type_soundness [library]
type_soundness [library]
type_soundness [library]
typofDecl [inductive, in framework.scopes]
typofDeclDet [lemma, in framework.scopes]
typofDecls [definition, in framework.scopes]
typofDeclsDet [lemma, in framework.scopes]
typofDecl_ [constructor, in framework.scopes]


U

uniqueDecls [projection, in framework.scopes]
uniqueRefs [projection, in framework.scopes]
UnitAV [constructor, in langs.L3.semantics]
UnitAV [constructor, in langs.L2.semantics]
UnitAV [constructor, in langs.L2.GCsemantics]
unreferenced [definition, in framework.GC]
unzip [definition, in langs.L2.syntax]
unzip [definition, in langs.L3.syntax]
unzipb [definition, in langs.L2.syntax]
unzipb [definition, in langs.L3.syntax]
unzipf [definition, in langs.L3.syntax]
unzipi [definition, in langs.L3.syntax]
upcast [inductive, in langs.L3.semantics]
upcast_scopeofFrame [lemma, in langs.L3.type_soundness]
upcast_up [constructor, in langs.L3.semantics]
upcast_ [constructor, in langs.L3.semantics]


V

V [inductive, in langs.L3.semantics]
V [inductive, in langs.L2.semantics]
V [inductive, in langs.L2.GCsemantics]
V [inductive, in langs.L1.semantics]
values_in [lemma, in framework.maps]
Var [constructor, in langs.L1.syntax]
Var [constructor, in langs.L2.syntax]
Var [constructor, in langs.L3.syntax]
VR [instance, in langs.L2.GCsemantics]
vrefers [projection, in framework.GC]
VRefers [record, in framework.GC]
VRefersProperties [section, in framework.GC]
vrefers' [inductive, in langs.L2.GCsemantics]
vr_record [constructor, in langs.L2.GCsemantics]
vr_deffun [constructor, in langs.L2.GCsemantics]
vr_clos [constructor, in langs.L2.GCsemantics]
VT [instance, in langs.L1.type_soundness]
VT [instance, in langs.L2.type_soundness]
VTR [instance, in langs.L2.GCtype_soundness]
vtyp [projection, in framework.frames]
VTyp [record, in framework.frames]
VTypProperties [section, in framework.frames]
VTypRefers [record, in framework.GC]
VTypRefersProperties [section, in framework.GC]
vtyp_ncc [constructor, in langs.L3.type_soundness]
vtyp_cc [constructor, in langs.L3.type_soundness]
vtyp' [inductive, in langs.L3.type_soundness]
vtyp' [inductive, in langs.L1.type_soundness]
vtyp' [inductive, in langs.L2.GCtype_soundness]
vtyp' [inductive, in langs.L2.type_soundness]
vtyp'_q [constructor, in langs.L3.type_soundness]
vtyp'_nr [constructor, in langs.L3.type_soundness]
vtyp'_r [constructor, in langs.L3.type_soundness]
vtyp'_df [constructor, in langs.L3.type_soundness]
vtyp'_f [constructor, in langs.L3.type_soundness]
vtyp'_b [constructor, in langs.L3.type_soundness]
vtyp'_n [constructor, in langs.L3.type_soundness]
vtyp'_c [constructor, in langs.L1.type_soundness]
vtyp'_n [constructor, in langs.L1.type_soundness]
vtyp'_q [constructor, in langs.L2.GCtype_soundness]
vtyp'_nr [constructor, in langs.L2.GCtype_soundness]
vtyp'_r [constructor, in langs.L2.GCtype_soundness]
vtyp'_df [constructor, in langs.L2.GCtype_soundness]
vtyp'_f [constructor, in langs.L2.GCtype_soundness]
vtyp'_b [constructor, in langs.L2.GCtype_soundness]
vtyp'_n [constructor, in langs.L2.GCtype_soundness]
vtyp'_q [constructor, in langs.L2.type_soundness]
vtyp'_nr [constructor, in langs.L2.type_soundness]
vtyp'_r [constructor, in langs.L2.type_soundness]
vtyp'_df [constructor, in langs.L2.type_soundness]
vtyp'_f [constructor, in langs.L2.type_soundness]
vtyp'_b [constructor, in langs.L2.type_soundness]
vtyp'_n [constructor, in langs.L2.type_soundness]
VT' [instance, in langs.L2.GCtype_soundness]
VT0 [instance, in langs.L3.type_soundness]


W

wb_prog_ [constructor, in langs.L2.well_boundness]
wb_prog [inductive, in langs.L2.well_boundness]
wb_rec_dec [constructor, in langs.L2.well_boundness]
wb_dec [inductive, in langs.L2.well_boundness]
wb_lhs_field [constructor, in langs.L2.well_boundness]
wb_lhs_var [constructor, in langs.L2.well_boundness]
wb_lhs [inductive, in langs.L2.well_boundness]
wb_new [constructor, in langs.L2.well_boundness]
wb_seq [constructor, in langs.L2.well_boundness]
wb_if [constructor, in langs.L2.well_boundness]
wb_asgn [constructor, in langs.L2.well_boundness]
wb_letrec [constructor, in langs.L2.well_boundness]
wb_letseq [constructor, in langs.L2.well_boundness]
wb_letpar [constructor, in langs.L2.well_boundness]
wb_app [constructor, in langs.L2.well_boundness]
wb_fn [constructor, in langs.L2.well_boundness]
wb_lhs_ [constructor, in langs.L2.well_boundness]
wb_gt [constructor, in langs.L2.well_boundness]
wb_plus [constructor, in langs.L2.well_boundness]
wb_cfalse [constructor, in langs.L2.well_boundness]
wb_ctrue [constructor, in langs.L2.well_boundness]
wb_cnum [constructor, in langs.L2.well_boundness]
wb_exp [inductive, in langs.L2.well_boundness]
wb_rec_dec [constructor, in langs.L2.well_typedness]
wb_prog_ [constructor, in langs.L3.well_boundness]
wb_prog [inductive, in langs.L3.well_boundness]
wb_decls_nil [constructor, in langs.L3.well_boundness]
wb_rec_decls [constructor, in langs.L3.well_boundness]
wb_decls [inductive, in langs.L3.well_boundness]
wb_lhs_field [constructor, in langs.L3.well_boundness]
wb_lhs_var [constructor, in langs.L3.well_boundness]
wb_lhs [inductive, in langs.L3.well_boundness]
wb_new [constructor, in langs.L3.well_boundness]
wb_seq [constructor, in langs.L3.well_boundness]
wb_if [constructor, in langs.L3.well_boundness]
wb_asgn [constructor, in langs.L3.well_boundness]
wb_letrec [constructor, in langs.L3.well_boundness]
wb_letseq [constructor, in langs.L3.well_boundness]
wb_letpar [constructor, in langs.L3.well_boundness]
wb_app [constructor, in langs.L3.well_boundness]
wb_fn [constructor, in langs.L3.well_boundness]
wb_lhs_ [constructor, in langs.L3.well_boundness]
wb_gt [constructor, in langs.L3.well_boundness]
wb_plus [constructor, in langs.L3.well_boundness]
wb_cfalse [constructor, in langs.L3.well_boundness]
wb_ctrue [constructor, in langs.L3.well_boundness]
wb_cnum [constructor, in langs.L3.well_boundness]
wb_exp [inductive, in langs.L3.well_boundness]
wb_representation_complete [lemma, in framework.frames]
wb_representation_sound [lemma, in framework.frames]
wb_prog_ [constructor, in langs.L1.well_boundness]
wb_prog [inductive, in langs.L1.well_boundness]
wb_app [constructor, in langs.L1.well_boundness]
wb_fn [constructor, in langs.L1.well_boundness]
wb_var [constructor, in langs.L1.well_boundness]
wb_plus [constructor, in langs.L1.well_boundness]
wb_cnum [constructor, in langs.L1.well_boundness]
wb_exp [inductive, in langs.L1.well_boundness]
WellBoundness [section, in langs.L2.well_boundness]
WellBoundness [section, in langs.L3.well_boundness]
WellBoundness [section, in langs.L1.well_boundness]
WellTypedness [section, in langs.L3.well_typedness]
WellTypedness [section, in langs.L2.well_typedness]
WellTypedness [section, in langs.L1.well_typedness]
well_bound_set [lemma, in framework.frames]
well_bound_get [lemma, in framework.frames]
well_typed_ [constructor, in framework.frames]
well_typed [inductive, in framework.frames]
well_bound_ [constructor, in framework.frames]
well_bound [inductive, in framework.frames]
well_typed_ [constructor, in framework.sub]
well_sub_typed [inductive, in framework.sub]
well_typedness [library]
well_typedness [library]
well_typedness [library]
well_boundness [library]
well_boundness [library]
well_boundness [library]
With [constructor, in langs.L3.syntax]
Wrong [constructor, in langs.L3.semantics]
Wrong [constructor, in langs.L2.semantics]
Wrong [constructor, in langs.L2.GCsemantics]
Wrong [constructor, in langs.L1.semantics]
wt_prog_ [constructor, in langs.L3.well_typedness]
wt_prog [inductive, in langs.L3.well_typedness]
wt_decl_nil [constructor, in langs.L3.well_typedness]
wt_decls_rec [constructor, in langs.L3.well_typedness]
wt_decls [inductive, in langs.L3.well_typedness]
wt_lhs_field [constructor, in langs.L3.well_typedness]
wt_lhs_var [constructor, in langs.L3.well_typedness]
wt_lhs [inductive, in langs.L3.well_typedness]
wt_new [constructor, in langs.L3.well_typedness]
wt_seq [constructor, in langs.L3.well_typedness]
wt_if [constructor, in langs.L3.well_typedness]
wt_asgn [constructor, in langs.L3.well_typedness]
wt_letrec [constructor, in langs.L3.well_typedness]
wt_letseq [constructor, in langs.L3.well_typedness]
wt_letpar [constructor, in langs.L3.well_typedness]
wt_app [constructor, in langs.L3.well_typedness]
wt_fn [constructor, in langs.L3.well_typedness]
wt_lhs_ [constructor, in langs.L3.well_typedness]
wt_gt [constructor, in langs.L3.well_typedness]
wt_plus [constructor, in langs.L3.well_typedness]
wt_cfalse [constructor, in langs.L3.well_typedness]
wt_ctrue [constructor, in langs.L3.well_typedness]
wt_cnum [constructor, in langs.L3.well_typedness]
wt_exp [inductive, in langs.L3.well_typedness]
wt_prog_ [constructor, in langs.L2.well_typedness]
wt_prog [inductive, in langs.L2.well_typedness]
wt_dec [inductive, in langs.L2.well_typedness]
wt_lhs_field [constructor, in langs.L2.well_typedness]
wt_lhs_var [constructor, in langs.L2.well_typedness]
wt_lhs [inductive, in langs.L2.well_typedness]
wt_new [constructor, in langs.L2.well_typedness]
wt_seq [constructor, in langs.L2.well_typedness]
wt_if [constructor, in langs.L2.well_typedness]
wt_asgn [constructor, in langs.L2.well_typedness]
wt_letrec [constructor, in langs.L2.well_typedness]
wt_letseq [constructor, in langs.L2.well_typedness]
wt_letpar [constructor, in langs.L2.well_typedness]
wt_app [constructor, in langs.L2.well_typedness]
wt_fn [constructor, in langs.L2.well_typedness]
wt_lhs_ [constructor, in langs.L2.well_typedness]
wt_gt [constructor, in langs.L2.well_typedness]
wt_plus [constructor, in langs.L2.well_typedness]
wt_cfalse [constructor, in langs.L2.well_typedness]
wt_ctrue [constructor, in langs.L2.well_typedness]
wt_cnum [constructor, in langs.L2.well_typedness]
wt_exp [inductive, in langs.L2.well_typedness]
wt_prog_ [constructor, in langs.L1.well_typedness]
wt_prog [inductive, in langs.L1.well_typedness]
wt_app [constructor, in langs.L1.well_typedness]
wt_fn [constructor, in langs.L1.well_typedness]
wt_var [constructor, in langs.L1.well_typedness]
wt_plus [constructor, in langs.L1.well_typedness]
wt_cnum [constructor, in langs.L1.well_typedness]
wt_exp [inductive, in langs.L1.well_typedness]



Variable Index

M

MapDomains.DecEq [in framework.maps]
Maps.Kdec [in framework.maps]



Library Index

F

frames


G

GC
GCsemantics
GCtype_soundness


M

maps


P

prop_fold


S

scopes
semantics
semantics
semantics
sub
syntax
syntax
syntax


T

type_soundness
type_soundness
type_soundness


W

well_typedness
well_typedness
well_typedness
well_boundness
well_boundness
well_boundness



Lemma Index

A

assocDataDet [in framework.scopes]
assocDataofRefDet [in framework.scopes]
assocScopeDet [in framework.scopes]
assocScopeofRefDet [in framework.scopes]


D

ddataofScopeDet [in framework.scopes]
ddataofScope_scopeofDecl [in framework.scopes]
Ddec [in framework.scopes]
declofRefDet [in framework.scopes]
declsofScopeDet [in framework.scopes]
declsofScope_scopeofDecl [in framework.scopes]
defaults_vtyp' [in framework.frames]
defaults_vtyp [in framework.frames]
default_vtyp' [in langs.L3.type_soundness]
default_vtyp' [in langs.L2.GCtype_soundness]
default_vtyp' [in langs.L2.type_soundness]
DomEq_set [in framework.maps]


E

ELdec [in framework.scopes]
emptyHeapNoFrames [in framework.frames]
eval_exp_scopeofFrame_aux [in langs.L3.type_soundness]
eval_exp_scopeofFrame [in langs.L1.type_soundness]
eval_exp_scopeofFrame_aux [in langs.L2.GCtype_soundness]
eval_exp_scopeofFrame_aux [in langs.L2.type_soundness]
exp_preservation [in langs.L3.type_soundness]
exp_preservation [in langs.L1.type_soundness]
exp_preservation [in langs.L2.GCtype_soundness]
exp_preservation [in langs.L2.type_soundness]


F

fillFrameDiff [in framework.frames]
fillFrameDiff' [in framework.frames]
fillFrameFrames [in framework.frames]
fillFrameSame [in framework.frames]
fillFrameSame' [in framework.frames]
fillFrameSlotDiff [in framework.frames]
fillFrameSlotDiff' [in framework.frames]
fillFrame_vtyp' [in langs.L3.type_soundness]
fillFrame_vtyp' [in langs.L1.type_soundness]
fillFrame_vtyp' [in langs.L2.GCtype_soundness]
fillFrame_vtyp' [in langs.L2.type_soundness]
forall2_in [in langs.L3.type_soundness]
forall2_sub_trans [in langs.L3.type_soundness]
FrameIdDec [in framework.frames]


G

getAddrDet [in framework.frames]
getAddr_good_frame_sub [in framework.sub]
getAddr_typofDecl_getSlot_sub [in framework.sub]
getAddr_getSlot_sub [in framework.sub]
getAddr_in_ds_sub [in framework.sub]
getAddr_scopeofFrame_sub [in framework.sub]
getRefDet [in framework.frames]
getSlotDet [in framework.frames]
getSlotFrame [in framework.frames]
get_empty [in framework.maps]
get_set_other [in framework.maps]
get_set_same [in framework.maps]
get_remove_other [in framework.maps]
get_remove_same [in framework.maps]
good_roots_decomp [in langs.L2.GCtype_soundness]
good_roots_drop2 [in langs.L2.GCtype_soundness]
good_roots_drop [in langs.L2.GCtype_soundness]
good_roots_swap [in langs.L2.GCtype_soundness]
good_frame_setSlot [in framework.frames]
good_frame_getSlot [in framework.frames]
good_addr [in framework.frames]
good_path [in framework.frames]
good_path0 [in framework.frames]
good_frame_getSlot_sub [in framework.sub]
good_frame_setSlot_sub [in framework.sub]
good_addr_sub [in framework.sub]
good_path_sub [in framework.sub]
good_heap2good_sub_heap [in framework.sub]
good_frame2good_sub_frame [in framework.sub]
good_heap_removeUnreachable [in framework.GC]
good_heap_removeAllUnreferenced [in framework.GC]
good_heap_removeUnreferenced [in framework.GC]
good_heap_safeRemoval [in framework.GC]


I

initDefaultDiff_scopeofFrame [in framework.frames]
initDefaultFrames [in framework.frames]
initDefaultSame_scopeofFrame [in framework.frames]
initDefault_good_roots [in langs.L2.GCtype_soundness]
initDefault_good_heap1 [in framework.frames]
initDefault_good_heap0 [in framework.frames]
initDefault_good_heap [in framework.frames]
initDefault_good_frame [in framework.frames]
initDefault_vtyp [in framework.frames]
initDefault_good_heap2_sub [in framework.sub]
initDefault_good_heap0_sub [in framework.sub]
initDefault_good_heap1_sub [in framework.sub]
initDefault_good_heap_sub [in framework.sub]
initDefault_good_frame_sub [in framework.sub]
initFrameDiff [in framework.frames]
initFrameDiff_scopeofFrame [in framework.frames]
initFrameDiff' [in framework.frames]
initFrameFrames [in framework.frames]
initFrameSame [in framework.frames]
initFrameSame_scopeofFrame [in framework.frames]
initFrameSlotDiff' [in framework.frames]
initFrame_good_heap2 [in framework.frames]
initFrame_good_heap1 [in framework.frames]
initFrame_good_heap0 [in framework.frames]
initFrame_good_heap [in framework.frames]
initFrame_good_frame [in framework.frames]
initFrame_well_typed [in framework.frames]
initFrame_well_bound2 [in framework.frames]
initFrame_well_bound1 [in framework.frames]
initFrame_well_bound [in framework.frames]
initFrame_other_good_frame [in framework.frames]
initFrame_other_well_typed [in framework.frames]
initFrame_other_well_bound [in framework.frames]
initFrame_vtyp [in framework.frames]
initFrame_good_heap_sub [in framework.sub]
initFrame_other_good_frame_sub [in framework.sub]
initFrame_other_well_typed_sub [in framework.sub]
initFrame_good_frame_sub [in framework.sub]
initFrame_well_typed_sub [in framework.sub]
init_decls_sound [in langs.L3.type_soundness]
in_2 [in langs.L3.type_soundness]
in_2 [in langs.L2.GCtype_soundness]
in_2 [in langs.L2.type_soundness]
in_keys_remove [in framework.maps]
in_keys_set [in framework.maps]
in_values [in framework.maps]
in_keys [in framework.maps]


K

keys_in [in framework.maps]


L

linksofFrameDet [in framework.frames]
linksofScopeDet [in framework.scopes]
llinksofFrameDet [in framework.frames]
llinksofScopeDet [in framework.scopes]
lookupDet [in framework.frames]


N

newFrameDiff [in framework.frames]
newFrameDiff' [in framework.frames]
newFrameFrames [in framework.frames]
newFrameNew [in framework.frames]
newFrameSame [in framework.frames]
newFrameSlotDiff [in framework.frames]
newFrameSlotDiff' [in framework.frames]
newFrameSlotSame [in framework.frames]
newFrame_vtyp' [in langs.L3.type_soundness]
newFrame_vtyp' [in langs.L1.type_soundness]
newFrame_vtyp' [in langs.L2.GCtype_soundness]
newFrame_vtyp' [in langs.L2.type_soundness]
not_keys_in [in framework.maps]
not_in_keys [in framework.maps]


P

pathofRefDet [in framework.scopes]
path_connectivity' [in framework.scopes]
prog_sound [in langs.L3.type_soundness]
prog_sound [in langs.L1.type_soundness]
prog_sound [in langs.L2.GCtype_soundness]
prog_sound [in langs.L2.type_soundness]


R

Rdec [in framework.scopes]
refsofScopeDet [in framework.scopes]
removeAllUnreachable_safe [in framework.GC]
removeAllUnreferenced_safe [in framework.GC]
removeFrameFrames [in framework.frames]
removeFrameFrames' [in framework.frames]
removeFrameFrames0 [in framework.frames]
removeFrameSame [in framework.frames]
removeFrameScope [in framework.frames]
removeFramesFrames [in framework.frames]
removeFrameSlot [in framework.frames]
removeFramesSame [in framework.frames]
removeFramesScope [in framework.frames]
removeFramesSlot [in framework.frames]
removeFrames_good_roots [in langs.L2.GCtype_soundness]
removeFrames_vtyp [in langs.L2.GCtype_soundness]
removeFrames_frefers [in framework.GC]
removeFrame_good_roots [in langs.L2.GCtype_soundness]
removeFrame_frefers [in framework.GC]
removeUnreferenced_safe [in framework.GC]
remove_in_keys [in framework.maps]
rlookupDet [in framework.scopes]


S

ScopeIdDec [in framework.scopes]
scopeofDeclDet [in framework.scopes]
scopeofDecl_sanity2 [in framework.scopes]
scopeofDecl_sanity1 [in framework.scopes]
scopeofFrameDet [in framework.frames]
scopeofFrameFrame [in framework.frames]
scopeofRefDet [in framework.scopes]
scopeofRef_sanity2 [in framework.scopes]
scopeofRef_sanity1 [in framework.scopes]
setSlotFrame [in framework.frames]
setSlotFrames [in framework.frames]
setSlotSame [in framework.frames]
setSlotScope [in framework.frames]
setSlotSlotDiff [in framework.frames]
setSlotSlotDiff' [in framework.frames]
setSlotSlotSame [in framework.frames]
setSlot_vtyp' [in langs.L3.type_soundness]
setSlot_vtyp' [in langs.L1.type_soundness]
setSlot_good_roots [in langs.L2.GCtype_soundness]
setSlot_vtyp' [in langs.L2.GCtype_soundness]
setSlot_vtyp' [in langs.L2.type_soundness]
setSlot_good_heap [in framework.frames]
setSlot_other_good_frame [in framework.frames]
setSlot_other_well_typed [in framework.frames]
setSlot_other_well_bound [in framework.frames]
setSlot_good_frame [in framework.frames]
setSlot_well_typed [in framework.frames]
setSlot_well_bound [in framework.frames]
setSlot_good_heap_sub [in framework.sub]
setSlot_good_sub_frame [in framework.sub]
setSlot_other_good_sub_frame [in framework.sub]
setSlot_other_well_sub_typed [in framework.sub]
setSlot_well_typed_sub [in framework.sub]
set_in_keys [in framework.maps]
slookupDet [in framework.scopes]
slookup_ddata [in framework.scopes]
slookup_declofPath [in framework.scopes]
slotsofFrameDet [in framework.frames]
sub_class_upcast [in langs.L3.type_soundness]
sub_tclassdef [in langs.L3.type_soundness]
sub_tclass [in langs.L3.type_soundness]
sub_tarrow [in langs.L3.type_soundness]
sub_bool [in langs.L3.type_soundness]
sub_int [in langs.L3.type_soundness]
sub'_refl [in langs.L3.type_soundness]
sub'_trans [in langs.L3.type_soundness]


T

typofDeclDet [in framework.scopes]
typofDeclsDet [in framework.scopes]


U

upcast_scopeofFrame [in langs.L3.type_soundness]


V

values_in [in framework.maps]


W

wb_representation_complete [in framework.frames]
wb_representation_sound [in framework.frames]
well_bound_set [in framework.frames]
well_bound_get [in framework.frames]



Constructor Index

A

AbortAV [in langs.L3.semantics]
AbortAV [in langs.L2.semantics]
AbortAV [in langs.L2.GCsemantics]
AbortV [in langs.L3.semantics]
AbortV [in langs.L2.semantics]
AbortV [in langs.L2.GCsemantics]
AbortV [in langs.L1.semantics]
AddrAV [in langs.L3.semantics]
AddrAV [in langs.L2.semantics]
AddrAV [in langs.L2.GCsemantics]
Addr_ [in framework.frames]
App [in langs.L1.syntax]
App [in langs.L2.syntax]
App [in langs.L3.syntax]
Asgn [in langs.L2.syntax]
Asgn [in langs.L3.syntax]
assign_refs_cons_b2 [in langs.L3.semantics]
assign_refs_cons_b1 [in langs.L3.semantics]
assign_refs_b2 [in langs.L3.semantics]
assign_refs_b1 [in langs.L3.semantics]
assign_refs_cons [in langs.L3.semantics]
assign_refs_nil [in langs.L3.semantics]
assocData_ [in framework.scopes]
assocScope_ [in framework.scopes]


B

Binder [in langs.L2.syntax]
Binder [in langs.L3.syntax]
BoolV [in langs.L3.semantics]
BoolV [in langs.L2.semantics]
BoolV [in langs.L2.GCsemantics]


C

Cdef [in langs.L3.syntax]
CFalse [in langs.L2.syntax]
CFalse [in langs.L3.syntax]
ClosV [in langs.L3.semantics]
ClosV [in langs.L2.semantics]
ClosV [in langs.L2.GCsemantics]
ClosV [in langs.L1.semantics]
CNum [in langs.L1.syntax]
CNum [in langs.L2.syntax]
CNum [in langs.L3.syntax]
ConstructorV [in langs.L3.semantics]
CTrue [in langs.L2.syntax]
CTrue [in langs.L3.syntax]


D

daunr [in framework.GC]
De [in framework.scopes]
declofRef_ [in framework.scopes]
defaults_nil [in framework.frames]
default_cons [in framework.frames]
DefFunV [in langs.L3.semantics]
DefFunV [in langs.L2.semantics]
DefFunV [in langs.L2.GCsemantics]
def_c [in langs.L3.type_soundness]
def_r [in langs.L3.type_soundness]
def_df [in langs.L3.type_soundness]
def_b [in langs.L3.type_soundness]
def_n [in langs.L3.type_soundness]
def_r [in langs.L2.GCtype_soundness]
def_df [in langs.L2.GCtype_soundness]
def_b [in langs.L2.GCtype_soundness]
def_n [in langs.L2.GCtype_soundness]
def_r [in langs.L2.type_soundness]
def_df [in langs.L2.type_soundness]
def_b [in langs.L2.type_soundness]
def_n [in langs.L2.type_soundness]
Dp [in framework.scopes]
ds [in framework.GC]
dunr [in framework.GC]
dunreach [in framework.GC]


E

E [in langs.L1.syntax]
E [in langs.L2.syntax]
E [in langs.L3.syntax]
Ep [in framework.scopes]
eval_prog_ [in langs.L3.semantics]
eval_objinit_orphan_b2 [in langs.L3.semantics]
eval_objinit_orphan_b1 [in langs.L3.semantics]
eval_objinit_orphan [in langs.L3.semantics]
eval_objinit_b5 [in langs.L3.semantics]
eval_objinit_b4 [in langs.L3.semantics]
eval_objinit_b3 [in langs.L3.semantics]
eval_objinit_b2 [in langs.L3.semantics]
eval_objinit_b1 [in langs.L3.semantics]
eval_objinit_null [in langs.L3.semantics]
eval_objinit_ [in langs.L3.semantics]
eval_lhs_field_b3 [in langs.L3.semantics]
eval_lhs_field_b2 [in langs.L3.semantics]
eval_lhs_field_b1 [in langs.L3.semantics]
eval_lhs_field_null [in langs.L3.semantics]
eval_lhs_field [in langs.L3.semantics]
eval_lhs_var_b [in langs.L3.semantics]
eval_lhs_var_ [in langs.L3.semantics]
eval_new_b1 [in langs.L3.semantics]
eval_new_ [in langs.L3.semantics]
eval_seq_b1 [in langs.L3.semantics]
eval_seq_ [in langs.L3.semantics]
eval_if_b1 [in langs.L3.semantics]
eval_if_f [in langs.L3.semantics]
eval_if_t [in langs.L3.semantics]
eval_asgn_b3 [in langs.L3.semantics]
eval_asgn_b2 [in langs.L3.semantics]
eval_asgn_b1 [in langs.L3.semantics]
eval_asgn_ [in langs.L3.semantics]
eval_letrec_b1 [in langs.L3.semantics]
eval_letrec_ [in langs.L3.semantics]
eval_letseq_b1 [in langs.L3.semantics]
eval_letseq_ [in langs.L3.semantics]
eval_letpar_b1 [in langs.L3.semantics]
eval_letpar_ [in langs.L3.semantics]
eval_app_b2 [in langs.L3.semantics]
eval_app_b1 [in langs.L3.semantics]
eval_app_dfun [in langs.L3.semantics]
eval_app [in langs.L3.semantics]
eval_fn_ [in langs.L3.semantics]
eval_lhs_b2 [in langs.L3.semantics]
eval_lhs_b1 [in langs.L3.semantics]
eval_lhs_ [in langs.L3.semantics]
eval_gt_b2 [in langs.L3.semantics]
eval_gt_b1 [in langs.L3.semantics]
eval_gt_ [in langs.L3.semantics]
eval_plus_b2 [in langs.L3.semantics]
eval_plus_b1 [in langs.L3.semantics]
eval_plus_ [in langs.L3.semantics]
eval_false_ [in langs.L3.semantics]
eval_true_ [in langs.L3.semantics]
eval_cnum_ [in langs.L3.semantics]
eval_prog_ [in langs.L2.semantics]
eval_lhs_field_b2 [in langs.L2.semantics]
eval_lhs_field_b1 [in langs.L2.semantics]
eval_lhs_field_null [in langs.L2.semantics]
eval_lhs_field [in langs.L2.semantics]
eval_lhs_var_b [in langs.L2.semantics]
eval_lhs_var_ [in langs.L2.semantics]
eval_new_b1 [in langs.L2.semantics]
eval_new_ [in langs.L2.semantics]
eval_seq_b1 [in langs.L2.semantics]
eval_seq_ [in langs.L2.semantics]
eval_if_b1 [in langs.L2.semantics]
eval_if_f [in langs.L2.semantics]
eval_if_t [in langs.L2.semantics]
eval_asgn_b3 [in langs.L2.semantics]
eval_asgn_b2 [in langs.L2.semantics]
eval_asgn_b1 [in langs.L2.semantics]
eval_asgn_ [in langs.L2.semantics]
eval_letrec_b1 [in langs.L2.semantics]
eval_letrec_ [in langs.L2.semantics]
eval_letseq_b1 [in langs.L2.semantics]
eval_letseq_ [in langs.L2.semantics]
eval_letpar_b1 [in langs.L2.semantics]
eval_letpar_ [in langs.L2.semantics]
eval_app_b2 [in langs.L2.semantics]
eval_app_b1 [in langs.L2.semantics]
eval_app_dfun [in langs.L2.semantics]
eval_app [in langs.L2.semantics]
eval_fn_ [in langs.L2.semantics]
eval_lhs_b2 [in langs.L2.semantics]
eval_lhs_b1 [in langs.L2.semantics]
eval_lhs_ [in langs.L2.semantics]
eval_gt_b2 [in langs.L2.semantics]
eval_gt_b1 [in langs.L2.semantics]
eval_gt_ [in langs.L2.semantics]
eval_plus_b2 [in langs.L2.semantics]
eval_plus_b1 [in langs.L2.semantics]
eval_plus_ [in langs.L2.semantics]
eval_false_ [in langs.L2.semantics]
eval_true_ [in langs.L2.semantics]
eval_cnum_ [in langs.L2.semantics]
eval_prog_ [in langs.L2.GCsemantics]
eval_lhs_field_b2 [in langs.L2.GCsemantics]
eval_lhs_field_b1 [in langs.L2.GCsemantics]
eval_lhs_field_null [in langs.L2.GCsemantics]
eval_lhs_field [in langs.L2.GCsemantics]
eval_lhs_var_b [in langs.L2.GCsemantics]
eval_lhs_var_ [in langs.L2.GCsemantics]
eval_new_b1 [in langs.L2.GCsemantics]
eval_new_ [in langs.L2.GCsemantics]
eval_seq_b1 [in langs.L2.GCsemantics]
eval_seq_ [in langs.L2.GCsemantics]
eval_if_b1 [in langs.L2.GCsemantics]
eval_if_f [in langs.L2.GCsemantics]
eval_if_t [in langs.L2.GCsemantics]
eval_asgn_b3 [in langs.L2.GCsemantics]
eval_asgn_b2 [in langs.L2.GCsemantics]
eval_asgn_b1 [in langs.L2.GCsemantics]
eval_asgn_ [in langs.L2.GCsemantics]
eval_letrec_b1 [in langs.L2.GCsemantics]
eval_letrec_ [in langs.L2.GCsemantics]
eval_letseq_b1 [in langs.L2.GCsemantics]
eval_letseq_ [in langs.L2.GCsemantics]
eval_letpar_b1 [in langs.L2.GCsemantics]
eval_letpar_ [in langs.L2.GCsemantics]
eval_app_b2 [in langs.L2.GCsemantics]
eval_app_b1 [in langs.L2.GCsemantics]
eval_app_dfun [in langs.L2.GCsemantics]
eval_app [in langs.L2.GCsemantics]
eval_fn_ [in langs.L2.GCsemantics]
eval_lhs_b2 [in langs.L2.GCsemantics]
eval_lhs_b1 [in langs.L2.GCsemantics]
eval_lhs_ [in langs.L2.GCsemantics]
eval_gt_b2 [in langs.L2.GCsemantics]
eval_gt_b1 [in langs.L2.GCsemantics]
eval_gt_ [in langs.L2.GCsemantics]
eval_plus_b2 [in langs.L2.GCsemantics]
eval_plus_b1 [in langs.L2.GCsemantics]
eval_plus_ [in langs.L2.GCsemantics]
eval_false_ [in langs.L2.GCsemantics]
eval_true_ [in langs.L2.GCsemantics]
eval_cnum_ [in langs.L2.GCsemantics]
eval_gc_ [in langs.L2.GCsemantics]
eval_prog_ [in langs.L1.semantics]
eval_app_b2 [in langs.L1.semantics]
eval_app_b1 [in langs.L1.semantics]
eval_app [in langs.L1.semantics]
eval_fn_ [in langs.L1.semantics]
eval_var_b2 [in langs.L1.semantics]
eval_var_b1 [in langs.L1.semantics]
eval_var_ [in langs.L1.semantics]
eval_plus_b2 [in langs.L1.semantics]
eval_plus_b1 [in langs.L1.semantics]
eval_plus_ [in langs.L1.semantics]
eval_cnum_ [in langs.L1.semantics]


F

Field [in langs.L2.syntax]
Field [in langs.L3.syntax]
fill_rec_cons_b2 [in langs.L3.semantics]
fill_rec_cons_b1 [in langs.L3.semantics]
fill_rec_cons [in langs.L3.semantics]
fill_rec_b2 [in langs.L3.semantics]
fill_rec_b1 [in langs.L3.semantics]
fill_rec_nil [in langs.L3.semantics]
fill_seq_cons_b2 [in langs.L3.semantics]
fill_seq_cons_b1 [in langs.L3.semantics]
fill_seq_cons [in langs.L3.semantics]
fill_seq_b2 [in langs.L3.semantics]
fill_seq_b1 [in langs.L3.semantics]
fill_seq_nil [in langs.L3.semantics]
fill_par_cons_b2 [in langs.L3.semantics]
fill_par_cons_b1 [in langs.L3.semantics]
fill_par_cons [in langs.L3.semantics]
fill_par_b2 [in langs.L3.semantics]
fill_par_b1 [in langs.L3.semantics]
fill_par_nil [in langs.L3.semantics]
fill_rec_cons_b2 [in langs.L2.semantics]
fill_rec_cons_b1 [in langs.L2.semantics]
fill_rec_cons [in langs.L2.semantics]
fill_rec_b2 [in langs.L2.semantics]
fill_rec_b1 [in langs.L2.semantics]
fill_rec_nil [in langs.L2.semantics]
fill_seq_cons_b2 [in langs.L2.semantics]
fill_seq_cons_b1 [in langs.L2.semantics]
fill_seq_cons [in langs.L2.semantics]
fill_seq_b2 [in langs.L2.semantics]
fill_seq_b1 [in langs.L2.semantics]
fill_seq_nil [in langs.L2.semantics]
fill_par_cons_b2 [in langs.L2.semantics]
fill_par_cons_b1 [in langs.L2.semantics]
fill_par_cons [in langs.L2.semantics]
fill_par_b2 [in langs.L2.semantics]
fill_par_b1 [in langs.L2.semantics]
fill_par_nil [in langs.L2.semantics]
fill_rec_cons_b2 [in langs.L2.GCsemantics]
fill_rec_cons_b1 [in langs.L2.GCsemantics]
fill_rec_cons [in langs.L2.GCsemantics]
fill_rec_b2 [in langs.L2.GCsemantics]
fill_rec_b1 [in langs.L2.GCsemantics]
fill_rec_nil [in langs.L2.GCsemantics]
fill_seq_cons_b2 [in langs.L2.GCsemantics]
fill_seq_cons_b1 [in langs.L2.GCsemantics]
fill_seq_cons [in langs.L2.GCsemantics]
fill_seq_b2 [in langs.L2.GCsemantics]
fill_seq_b1 [in langs.L2.GCsemantics]
fill_seq_nil [in langs.L2.GCsemantics]
fill_par_cons_b2 [in langs.L2.GCsemantics]
fill_par_cons_b1 [in langs.L2.GCsemantics]
fill_par_cons [in langs.L2.GCsemantics]
fill_par_b2 [in langs.L2.GCsemantics]
fill_par_b1 [in langs.L2.GCsemantics]
fill_par_nil [in langs.L2.GCsemantics]
Flddecl [in langs.L2.syntax]
FldDecl [in langs.L3.syntax]
Fn [in langs.L1.syntax]
Fn [in langs.L2.syntax]
Fn [in langs.L3.syntax]
ForallFold2_cons [in framework.prop_fold]
ForallFold2_nil [in framework.prop_fold]
FrameAV [in langs.L3.semantics]
FrameAV [in langs.L2.semantics]
FrameAV [in langs.L2.GCsemantics]
fr_slot [in framework.GC]
fr_link [in framework.GC]


G

getAddr_ [in framework.frames]
getRef_ [in framework.frames]
getSlots_ [in framework.frames]
getSlot_ [in framework.frames]
Gt [in langs.L2.syntax]
Gt [in langs.L3.syntax]


I

I [in framework.scopes]
If [in langs.L2.syntax]
If [in langs.L3.syntax]
initDefault_ [in framework.frames]
initFrame_ [in framework.frames]
Initializer [in langs.L3.syntax]
init_decl_nil [in langs.L3.semantics]
init_decl_rdef [in langs.L3.semantics]


L

LetPar [in langs.L2.syntax]
LetPar [in langs.L3.syntax]
LetRec [in langs.L2.syntax]
LetRec [in langs.L3.syntax]
LetSeq [in langs.L2.syntax]
LetSeq [in langs.L3.syntax]
Lhs [in langs.L2.syntax]
Lhs [in langs.L3.syntax]
linksofFrame_ [in framework.frames]
llinksofFrame_ [in framework.frames]
lookupD [in framework.frames]
lookupI [in framework.frames]


N

New [in langs.L2.syntax]
New [in langs.L3.syntax]
NullPointer [in langs.L3.semantics]
NullPointer [in langs.L2.semantics]
NullPointer [in langs.L2.GCsemantics]
NullV [in langs.L3.semantics]
NullV [in langs.L2.semantics]
NullV [in langs.L2.GCsemantics]
NumV [in langs.L3.semantics]
NumV [in langs.L2.semantics]
NumV [in langs.L2.GCsemantics]
NumV [in langs.L1.semantics]


O

ObjectV [in langs.L3.semantics]


P

P [in framework.scopes]
Plus [in langs.L1.syntax]
Plus [in langs.L2.syntax]
Plus [in langs.L3.syntax]
Prog [in langs.L1.syntax]
Prog [in langs.L2.syntax]
Prog [in langs.L3.syntax]


R

Rdef [in langs.L2.syntax]
Re [in framework.scopes]
RecordV [in langs.L2.semantics]
RecordV [in langs.L2.GCsemantics]
re_fref [in framework.GC]
re_refl [in framework.GC]
rfs_cons [in framework.frames]
rfs_nil [in framework.frames]


S

scopeofFrame_ [in framework.frames]
Seq [in langs.L2.syntax]
Seq [in langs.L3.syntax]
setSlot_ [in framework.frames]
sub_fun [in langs.L3.well_typedness]
sub_rec [in langs.L3.well_typedness]
sub'_trans [in langs.L3.well_typedness]
sub'_refl [in langs.L3.well_typedness]


T

Tarrow [in langs.L1.syntax]
Tarrow [in langs.L2.syntax]
Tarrow [in langs.L3.syntax]
Tbool [in langs.L2.syntax]
Tbool [in langs.L3.syntax]
Tclass [in langs.L3.syntax]
TclassDef [in langs.L3.syntax]
Tint [in langs.L1.syntax]
Tint [in langs.L2.syntax]
Tint [in langs.L3.syntax]
Trecord [in langs.L2.syntax]
typofDecl_ [in framework.scopes]


U

UnitAV [in langs.L3.semantics]
UnitAV [in langs.L2.semantics]
UnitAV [in langs.L2.GCsemantics]
upcast_up [in langs.L3.semantics]
upcast_ [in langs.L3.semantics]


V

Var [in langs.L1.syntax]
Var [in langs.L2.syntax]
Var [in langs.L3.syntax]
vr_record [in langs.L2.GCsemantics]
vr_deffun [in langs.L2.GCsemantics]
vr_clos [in langs.L2.GCsemantics]
vtyp_ncc [in langs.L3.type_soundness]
vtyp_cc [in langs.L3.type_soundness]
vtyp'_q [in langs.L3.type_soundness]
vtyp'_nr [in langs.L3.type_soundness]
vtyp'_r [in langs.L3.type_soundness]
vtyp'_df [in langs.L3.type_soundness]
vtyp'_f [in langs.L3.type_soundness]
vtyp'_b [in langs.L3.type_soundness]
vtyp'_n [in langs.L3.type_soundness]
vtyp'_c [in langs.L1.type_soundness]
vtyp'_n [in langs.L1.type_soundness]
vtyp'_q [in langs.L2.GCtype_soundness]
vtyp'_nr [in langs.L2.GCtype_soundness]
vtyp'_r [in langs.L2.GCtype_soundness]
vtyp'_df [in langs.L2.GCtype_soundness]
vtyp'_f [in langs.L2.GCtype_soundness]
vtyp'_b [in langs.L2.GCtype_soundness]
vtyp'_n [in langs.L2.GCtype_soundness]
vtyp'_q [in langs.L2.type_soundness]
vtyp'_nr [in langs.L2.type_soundness]
vtyp'_r [in langs.L2.type_soundness]
vtyp'_df [in langs.L2.type_soundness]
vtyp'_f [in langs.L2.type_soundness]
vtyp'_b [in langs.L2.type_soundness]
vtyp'_n [in langs.L2.type_soundness]


W

wb_prog_ [in langs.L2.well_boundness]
wb_rec_dec [in langs.L2.well_boundness]
wb_lhs_field [in langs.L2.well_boundness]
wb_lhs_var [in langs.L2.well_boundness]
wb_new [in langs.L2.well_boundness]
wb_seq [in langs.L2.well_boundness]
wb_if [in langs.L2.well_boundness]
wb_asgn [in langs.L2.well_boundness]
wb_letrec [in langs.L2.well_boundness]
wb_letseq [in langs.L2.well_boundness]
wb_letpar [in langs.L2.well_boundness]
wb_app [in langs.L2.well_boundness]
wb_fn [in langs.L2.well_boundness]
wb_lhs_ [in langs.L2.well_boundness]
wb_gt [in langs.L2.well_boundness]
wb_plus [in langs.L2.well_boundness]
wb_cfalse [in langs.L2.well_boundness]
wb_ctrue [in langs.L2.well_boundness]
wb_cnum [in langs.L2.well_boundness]
wb_rec_dec [in langs.L2.well_typedness]
wb_prog_ [in langs.L3.well_boundness]
wb_decls_nil [in langs.L3.well_boundness]
wb_rec_decls [in langs.L3.well_boundness]
wb_lhs_field [in langs.L3.well_boundness]
wb_lhs_var [in langs.L3.well_boundness]
wb_new [in langs.L3.well_boundness]
wb_seq [in langs.L3.well_boundness]
wb_if [in langs.L3.well_boundness]
wb_asgn [in langs.L3.well_boundness]
wb_letrec [in langs.L3.well_boundness]
wb_letseq [in langs.L3.well_boundness]
wb_letpar [in langs.L3.well_boundness]
wb_app [in langs.L3.well_boundness]
wb_fn [in langs.L3.well_boundness]
wb_lhs_ [in langs.L3.well_boundness]
wb_gt [in langs.L3.well_boundness]
wb_plus [in langs.L3.well_boundness]
wb_cfalse [in langs.L3.well_boundness]
wb_ctrue [in langs.L3.well_boundness]
wb_cnum [in langs.L3.well_boundness]
wb_prog_ [in langs.L1.well_boundness]
wb_app [in langs.L1.well_boundness]
wb_fn [in langs.L1.well_boundness]
wb_var [in langs.L1.well_boundness]
wb_plus [in langs.L1.well_boundness]
wb_cnum [in langs.L1.well_boundness]
well_typed_ [in framework.frames]
well_bound_ [in framework.frames]
well_typed_ [in framework.sub]
With [in langs.L3.syntax]
Wrong [in langs.L3.semantics]
Wrong [in langs.L2.semantics]
Wrong [in langs.L2.GCsemantics]
Wrong [in langs.L1.semantics]
wt_prog_ [in langs.L3.well_typedness]
wt_decl_nil [in langs.L3.well_typedness]
wt_decls_rec [in langs.L3.well_typedness]
wt_lhs_field [in langs.L3.well_typedness]
wt_lhs_var [in langs.L3.well_typedness]
wt_new [in langs.L3.well_typedness]
wt_seq [in langs.L3.well_typedness]
wt_if [in langs.L3.well_typedness]
wt_asgn [in langs.L3.well_typedness]
wt_letrec [in langs.L3.well_typedness]
wt_letseq [in langs.L3.well_typedness]
wt_letpar [in langs.L3.well_typedness]
wt_app [in langs.L3.well_typedness]
wt_fn [in langs.L3.well_typedness]
wt_lhs_ [in langs.L3.well_typedness]
wt_gt [in langs.L3.well_typedness]
wt_plus [in langs.L3.well_typedness]
wt_cfalse [in langs.L3.well_typedness]
wt_ctrue [in langs.L3.well_typedness]
wt_cnum [in langs.L3.well_typedness]
wt_prog_ [in langs.L2.well_typedness]
wt_lhs_field [in langs.L2.well_typedness]
wt_lhs_var [in langs.L2.well_typedness]
wt_new [in langs.L2.well_typedness]
wt_seq [in langs.L2.well_typedness]
wt_if [in langs.L2.well_typedness]
wt_asgn [in langs.L2.well_typedness]
wt_letrec [in langs.L2.well_typedness]
wt_letseq [in langs.L2.well_typedness]
wt_letpar [in langs.L2.well_typedness]
wt_app [in langs.L2.well_typedness]
wt_fn [in langs.L2.well_typedness]
wt_lhs_ [in langs.L2.well_typedness]
wt_gt [in langs.L2.well_typedness]
wt_plus [in langs.L2.well_typedness]
wt_cfalse [in langs.L2.well_typedness]
wt_ctrue [in langs.L2.well_typedness]
wt_cnum [in langs.L2.well_typedness]
wt_prog_ [in langs.L1.well_typedness]
wt_app [in langs.L1.well_typedness]
wt_fn [in langs.L1.well_typedness]
wt_var [in langs.L1.well_typedness]
wt_plus [in langs.L1.well_typedness]
wt_cnum [in langs.L1.well_typedness]



Inductive Index

A

Addr [in framework.frames]
assign_refs [in langs.L3.semantics]
assocData [in framework.scopes]
assocScope [in framework.scopes]
AuxV [in langs.L3.semantics]
AuxV [in langs.L2.semantics]
AuxV [in langs.L2.GCsemantics]


B

binder [in langs.L2.syntax]
binder [in langs.L3.syntax]


D

D [in framework.scopes]
decl [in langs.L2.syntax]
decl [in langs.L3.syntax]
declofRef [in framework.scopes]
default [in langs.L3.type_soundness]
default [in langs.L2.GCtype_soundness]
default [in langs.L2.type_soundness]
defaults [in framework.frames]


E

EdgeLabel [in framework.scopes]
Error [in langs.L3.semantics]
Error [in langs.L2.semantics]
Error [in langs.L2.GCsemantics]
Error [in langs.L1.semantics]
eval_prog [in langs.L3.semantics]
eval_objinit [in langs.L3.semantics]
eval_lhs [in langs.L3.semantics]
eval_exp [in langs.L3.semantics]
eval_prog [in langs.L2.semantics]
eval_lhs [in langs.L2.semantics]
eval_exp [in langs.L2.semantics]
eval_prog [in langs.L2.GCsemantics]
eval_lhs [in langs.L2.GCsemantics]
eval_exp [in langs.L2.GCsemantics]
eval_prog [in langs.L1.semantics]
eval_exp [in langs.L1.semantics]
exp [in langs.L1.syntax]
exp [in langs.L2.syntax]
exp [in langs.L3.syntax]


F

fill_slots_rec [in langs.L3.semantics]
fill_slots_seq [in langs.L3.semantics]
fill_slots_par [in langs.L3.semantics]
fill_slots_rec [in langs.L2.semantics]
fill_slots_seq [in langs.L2.semantics]
fill_slots_par [in langs.L2.semantics]
fill_slots_rec [in langs.L2.GCsemantics]
fill_slots_seq [in langs.L2.GCsemantics]
fill_slots_par [in langs.L2.GCsemantics]
fld_decl [in langs.L2.syntax]
fld_decl [in langs.L3.syntax]
ForallFold2 [in framework.prop_fold]
frefers [in framework.GC]


G

getAddr [in framework.frames]
getRef [in framework.frames]
getSlot [in framework.frames]


I

initDefault [in framework.frames]
initFrame [in framework.frames]
initializer [in langs.L3.syntax]
init_decls [in langs.L3.semantics]


L

lhs [in langs.L2.syntax]
lhs [in langs.L3.syntax]
linksofFrame [in framework.frames]
llinksofFrame [in framework.frames]
lookup [in framework.frames]


P

path [in framework.scopes]
pre_exp [in langs.L1.syntax]
pre_exp [in langs.L2.syntax]
pre_exp [in langs.L3.syntax]
prog [in langs.L1.syntax]
prog [in langs.L2.syntax]
prog [in langs.L3.syntax]


R

R [in framework.scopes]
reachable [in framework.GC]
removeAllUnreachable [in framework.GC]
removeAllUnreferenced [in framework.GC]
removeFrames [in framework.frames]
removeUnreferenced [in framework.GC]


S

safeRemoval [in framework.GC]
scopeofFrame [in framework.frames]
setSlot [in framework.frames]
slotsofFrame [in framework.frames]
sub' [in langs.L3.well_typedness]
sub1 [in langs.L3.well_typedness]


T

T [in langs.L1.syntax]
T [in langs.L2.syntax]
T [in langs.L3.syntax]
typofDecl [in framework.scopes]


U

upcast [in langs.L3.semantics]


V

V [in langs.L3.semantics]
V [in langs.L2.semantics]
V [in langs.L2.GCsemantics]
V [in langs.L1.semantics]
vrefers' [in langs.L2.GCsemantics]
vtyp' [in langs.L3.type_soundness]
vtyp' [in langs.L1.type_soundness]
vtyp' [in langs.L2.GCtype_soundness]
vtyp' [in langs.L2.type_soundness]


W

wb_prog [in langs.L2.well_boundness]
wb_dec [in langs.L2.well_boundness]
wb_lhs [in langs.L2.well_boundness]
wb_exp [in langs.L2.well_boundness]
wb_prog [in langs.L3.well_boundness]
wb_decls [in langs.L3.well_boundness]
wb_lhs [in langs.L3.well_boundness]
wb_exp [in langs.L3.well_boundness]
wb_prog [in langs.L1.well_boundness]
wb_exp [in langs.L1.well_boundness]
well_typed [in framework.frames]
well_bound [in framework.frames]
well_sub_typed [in framework.sub]
wt_prog [in langs.L3.well_typedness]
wt_decls [in langs.L3.well_typedness]
wt_lhs [in langs.L3.well_typedness]
wt_exp [in langs.L3.well_typedness]
wt_prog [in langs.L2.well_typedness]
wt_dec [in langs.L2.well_typedness]
wt_lhs [in langs.L2.well_typedness]
wt_exp [in langs.L2.well_typedness]
wt_prog [in langs.L1.well_typedness]
wt_exp [in langs.L1.well_typedness]



Projection Index

D

default [in framework.frames]
default_vtyp [in framework.frames]


F

fillFrame_vtyp [in framework.frames]


G

g [in framework.scopes]


N

newFrame_vtyp [in framework.frames]


P

path_connectivity [in framework.scopes]


R

removeFrames_vtyp [in framework.GC]


S

setSlot_vtyp [in framework.frames]
sub [in framework.sub]
sub_trans [in framework.sub]
sub_refl [in framework.sub]


U

uniqueDecls [in framework.scopes]
uniqueRefs [in framework.scopes]


V

vrefers [in framework.GC]
vtyp [in framework.frames]



Section Index

D

DefaultVTypProperties [in framework.frames]
DynamicSemantics [in langs.L3.semantics]
DynamicSemantics [in langs.L2.semantics]
DynamicSemantics [in langs.L2.GCsemantics]
DynamicSemantics [in langs.L1.semantics]


F

FrameHeapProperties [in framework.frames]
FrameHeapProperties.CombiningStaticAndDynamic [in framework.frames]


G

Goodness [in framework.frames]


L

LookupPredicates [in framework.scopes]


M

MapDomains [in framework.maps]
Maps [in framework.maps]


P

PredicateForms [in framework.scopes]


R

RGATProperties [in framework.scopes]


S

SanityChecks [in framework.scopes]


T

TV [in framework.sub]
TypeSoundness [in langs.L3.type_soundness]
TypeSoundness [in langs.L1.type_soundness]
TypeSoundness [in langs.L2.GCtype_soundness]
TypeSoundness [in langs.L2.type_soundness]


V

VRefersProperties [in framework.GC]
VTypProperties [in framework.frames]
VTypRefersProperties [in framework.GC]


W

WellBoundness [in langs.L2.well_boundness]
WellBoundness [in langs.L3.well_boundness]
WellBoundness [in langs.L1.well_boundness]
WellTypedness [in langs.L3.well_typedness]
WellTypedness [in langs.L2.well_typedness]
WellTypedness [in langs.L1.well_typedness]



Instance Index

D

DVT [in langs.L3.type_soundness]
DVT [in langs.L2.type_soundness]
DVT' [in langs.L2.GCtype_soundness]


F

FH [in langs.L3.type_soundness]
FH [in langs.L2.GCtype_soundness]
FH [in langs.L2.type_soundness]
FH [in langs.L1.semantics]


S

ST [in langs.L3.type_soundness]


V

VR [in langs.L2.GCsemantics]
VT [in langs.L1.type_soundness]
VT [in langs.L2.type_soundness]
VTR [in langs.L2.GCtype_soundness]
VT' [in langs.L2.GCtype_soundness]
VT0 [in langs.L3.type_soundness]



Definition Index

A

aabort [in langs.L3.semantics]
aaborta [in langs.L3.semantics]
abort [in langs.L3.semantics]
abort [in langs.L2.semantics]
abort [in langs.L2.GCsemantics]
abort [in langs.L1.semantics]
aborta [in langs.L3.semantics]
aborta [in langs.L2.semantics]
aborta [in langs.L2.GCsemantics]
assign_refs_scopeofFrame [in langs.L3.type_soundness]
assign_refs_ind2 [in langs.L3.semantics]
assocDataofRef [in framework.scopes]
assocScopeofRef [in framework.scopes]
AT [in framework.scopes]


D

ddataofScopeP [in framework.scopes]
declofPath [in framework.scopes]
declsofScopeP [in framework.scopes]
DomEq [in framework.maps]


E

empty [in framework.maps]
emptyHeap [in framework.frames]
eval_objinit_scopeofFrame [in langs.L3.type_soundness]
eval_lhs_scopeofFrame [in langs.L3.type_soundness]
eval_exp_scopeofFrame [in langs.L3.type_soundness]
eval_exp_ind3 [in langs.L3.semantics]
eval_objinit_ind2 [in langs.L3.semantics]
eval_lhs_ind2 [in langs.L3.semantics]
eval_exp_ind2 [in langs.L3.semantics]
eval_lhs_scopeofFrame [in langs.L2.GCtype_soundness]
eval_exp_scopeofFrame [in langs.L2.GCtype_soundness]
eval_exp_ind3 [in langs.L2.semantics]
eval_lhs_ind2 [in langs.L2.semantics]
eval_exp_ind2 [in langs.L2.semantics]
eval_lhs_scopeofFrame [in langs.L2.type_soundness]
eval_exp_scopeofFrame [in langs.L2.type_soundness]
eval_exp_ind3 [in langs.L2.GCsemantics]
eval_lhs_ind2 [in langs.L2.GCsemantics]
eval_exp_ind2 [in langs.L2.GCsemantics]
expScope [in langs.L1.syntax]
expScope [in langs.L2.syntax]
expScope [in langs.L3.syntax]
expType [in langs.L1.syntax]
expType [in langs.L2.syntax]
expType [in langs.L3.syntax]


F

fillFrame [in framework.frames]
fill_rec_scopeofFrame [in langs.L3.type_soundness]
fill_seq_scopeofFrame [in langs.L3.type_soundness]
fill_par_scopeofFrame [in langs.L3.type_soundness]
fill_rec_ind2 [in langs.L3.semantics]
fill_seq_ind2 [in langs.L3.semantics]
fill_par_ind2 [in langs.L3.semantics]
fill_rec_scopeofFrame [in langs.L2.GCtype_soundness]
fill_seq_scopeofFrame [in langs.L2.GCtype_soundness]
fill_par_scopeofFrame [in langs.L2.GCtype_soundness]
fill_rec_ind2 [in langs.L2.semantics]
fill_seq_ind2 [in langs.L2.semantics]
fill_par_ind2 [in langs.L2.semantics]
fill_rec_scopeofFrame [in langs.L2.type_soundness]
fill_seq_scopeofFrame [in langs.L2.type_soundness]
fill_par_scopeofFrame [in langs.L2.type_soundness]
fill_rec_ind2 [in langs.L2.GCsemantics]
fill_seq_ind2 [in langs.L2.GCsemantics]
fill_par_ind2 [in langs.L2.GCsemantics]
fldDecl [in langs.L2.syntax]
fldDT [in langs.L3.syntax]
fldI [in langs.L3.syntax]
fldType [in langs.L2.syntax]
frame [in framework.frames]
FrameId [in framework.frames]


G

get [in framework.maps]
good [in langs.L3.semantics]
good [in langs.L2.semantics]
good [in langs.L2.GCsemantics]
good [in langs.L1.semantics]
good_roots [in langs.L2.GCtype_soundness]
good_heap [in framework.frames]
good_frame [in framework.frames]
good_sub_heap [in framework.sub]
good_sub_frame [in framework.sub]


I

ident [in framework.scopes]
initExp [in langs.L3.syntax]
initRef [in langs.L3.syntax]
is_val [in langs.L2.syntax]
is_val [in langs.L3.syntax]


K

keys [in framework.maps]


L

linksofScopeP [in framework.scopes]
llinksofScopeP [in framework.scopes]


M

map [in framework.maps]


N

newFrame [in framework.frames]


P

pathofRefP [in framework.scopes]


R

refsofScopeP [in framework.scopes]
remove [in framework.maps]
removeFrame [in framework.frames]
rlookup [in framework.scopes]


S

ScopeId [in framework.scopes]
scopeofDeclP [in framework.scopes]
scopeofRefP [in framework.scopes]
set [in framework.maps]
split_b [in langs.L2.syntax]
split_f [in langs.L3.syntax]
split_i [in langs.L3.syntax]
split_b [in langs.L3.syntax]


T

typofDecls [in framework.scopes]


U

unreferenced [in framework.GC]
unzip [in langs.L2.syntax]
unzip [in langs.L3.syntax]
unzipb [in langs.L2.syntax]
unzipb [in langs.L3.syntax]
unzipf [in langs.L3.syntax]
unzipi [in langs.L3.syntax]



Record Index

D

DefaultVTyp [in framework.frames]


F

FrameHeap [in framework.frames]


G

Graph [in framework.scopes]


S

SubTyping [in framework.sub]


V

VRefers [in framework.GC]
VTyp [in framework.frames]
VTypRefers [in framework.GC]



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 _ other (1032 entries)
Variable 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 _ other (2 entries)
Library 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 _ other (23 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 _ other (222 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 _ other (494 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 _ other (118 entries)
Projection 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 _ other (15 entries)
Section 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 _ other (28 entries)
Instance 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 _ other (14 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 _ other (109 entries)
Record 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 _ other (7 entries)

This page has been generated by coqdoc