component | plane | files |
|
examples | terms with special features | levels_ex0ty3_ex1nf2_ex2 |
|
| | |
|
dynamic typing | well-formed contexts | wf3_defs | wf3_props |
| context ref. for native type assignment | csubt_defs | csubt_propscsubt_arity_props |
| native type assignment | ty3_defs | ty3_propsty3_genty3_gen_contextty3_gen_nf2ty3_liftty3_subst0ty3_arity_propsty3_nf2_genty3_sredty3_sred_propsty3_dec |
equivalence | context-sensitive equivalence | pc3_defs | pc3_propspc3_genpc3_gen_contextpc3_subst0 |
| context-free equivalence | pc1_defs | pc1_props |
| | |
|
computation | context ref. for reducibility | csubc_defs | csubc_props |
| reducibility | sc3_defs | sc3_propssc3_arity |
| strongly normalizing computation | sn3_defs | sn3_gensn3_props |
| context-sensitive computation | pr3_defs | pr3_propspr3_genpr3_gen_contextpr3_isopr3_subst1pr3_confluence |
| context-free computation | pr1_defs | pr1_propspr1_confluence |
reduction | normal forms for context-sensitive reduction | nf2_defs | nf2_propsnf2_gennf2_dec |
| context-sensitive reduction | pr2_defs | pr2_genpr2_gen_contextpr2_liftpr2_subst1pr2_confluence |
| normal forms for context-free reduction | | nf0_dec |
| context-free reduction | wcpr0_defs |
|
|
| pr0_defs | pr0_genpr0_liftpr0_subst0pr0_subst1pr0_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_propsarity_genarity_subst0arity_sred |
| binary arity | levels_defsllt_defsaprem_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_gensubst1_liftsubst1_subst1subst1_confluence |
| normal forms for ordinary strict substitution | | dnf_dec |
| ordinary strict substitution | fsubst0_defs |
|
|
| csubst0_defs |
|
|
| subst0_defs | subst0_gensubst0_tltsubst0_liftsubst0_subst0subst0_confluence |
| basic local env. slicing | getl_defs | getl_props |
|
| drop_defs | drop_props |
| basic term relocation | lift_defs | lift_propslift_genlift_tlt |
grammar | closures | flt_defs |
|
| contexts | contexts_defsclt_defsctail_defsapp_defscnt_defs |
|
| terms | tlist_defs |
|
|
| terms_defstlt_defsiso_defs |
|