home	news	documentation	specification			implementation
foreword	milestones	version 2	version 2	(background - core - applications)		library	(static LDDL directory)
citations	visibility	version 1	version 1	(core)	(static HELM directory)	helena

Here is a numerical account of the specification's contents and its timeline.

This table reports the specification's components and their planes.

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