component |
plane |
files |
|
examples |
terms with special features |
levels_ex0
ty3_ex1
nf2_ex2
|
|
|
|
|
|
dynamic typing |
well-formed contexts |
wf3_defs
|
wf3_props
|
|
context ref. for native type assignment |
csubt_defs
|
csubt_props
csubt_arity_props
|
|
native type assignment |
ty3_defs
|
ty3_props
ty3_gen
ty3_gen_context
ty3_gen_nf2
ty3_lift
ty3_subst0
ty3_arity_props
ty3_nf2_gen
ty3_sred
ty3_sred_props
ty3_dec
|
equivalence |
context-sensitive equivalence |
pc3_defs
|
pc3_props
pc3_gen
pc3_gen_context
pc3_subst0
|
|
context-free equivalence |
pc1_defs
|
pc1_props
|
|
|
|
|
computation |
context ref. for reducibility |
csubc_defs
|
csubc_props
|
|
reducibility |
sc3_defs
|
sc3_props
sc3_arity
|
|
strongly normalizing computation |
sn3_defs
|
sn3_gen
sn3_props
|
|
context-sensitive computation |
pr3_defs
|
pr3_props
pr3_gen
pr3_gen_context
pr3_iso
pr3_subst1
pr3_confluence
|
|
context-free computation |
pr1_defs
|
pr1_props
pr1_confluence
|
reduction |
normal forms for context-sensitive reduction |
nf2_defs
|
nf2_props
nf2_gen
nf2_dec
|
|
context-sensitive reduction |
pr2_defs
|
pr2_gen
pr2_gen_context
pr2_lift
pr2_subst1
pr2_confluence
|
|
normal forms for context-free reduction |
|
nf0_dec
|
|
context-free reduction |
wcpr0_defs
|
|
|
|
pr0_defs
|
pr0_gen
pr0_lift
pr0_subst0
pr0_subst1
pr0_confluence
|
unfold |
iterated static type assignment |
sty1_defs
|
sty1_props
|
static typing |
static type assignment |
sty0_defs
|
sty0_props
|
|
context ref. for binary arity assignment |
csuba_defs
|
csuba_props
|
|
binary arity assignment |
arity_defs
|
arity_props
arity_gen
arity_subst0
arity_sred
|
|
binary arity |
levels_defs
llt_defs
aprem_defs
|
|
|
parameters |
parameter_defs
|
|
|
basic context ref. |
csubv_defs
|
|
multiple substitution |
iterated context slicing |
drop1_defs
|
drop1_props
|
|
generic term relocation |
lift1_defs
|
lift1_props
|
substitution |
ordinary substitution |
subst_defs
|
subst_props
|
|
|
csubst1_defs
|
csubst1_props
|
|
|
subst1_defs
|
subst1_gen
subst1_lift
subst1_subst1
subst1_confluence
|
|
normal forms for ordinary strict substitution |
|
dnf_dec
|
|
ordinary strict substitution |
fsubst0_defs
|
|
|
|
csubst0_defs
|
|
|
|
subst0_defs
|
subst0_gen
subst0_tlt
subst0_lift
subst0_subst0
subst0_confluence
|
|
basic local env. slicing |
getl_defs
|
getl_props
|
|
|
drop_defs
|
drop_props
|
|
basic term relocation |
lift_defs
|
lift_props
lift_gen
lift_tlt
|
grammar |
closures |
flt_defs
|
|
|
contexts |
contexts_defs
clt_defs
ctail_defs
app_defs
cnt_defs
|
|
|
terms |
tlist_defs
|
|
|
|
terms_defs
tlt_defs
iso_defs
|
|