\lambda\delta home page

[lambdadelta home]

cic:/matita/lambdadelta/basic_2/ (core λδ version 2)

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

Summary of the Specification [spacer]

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

category	objects
sizes	files	83	characters	55955	nodes	191279
propositions	theorems	33	lemmas	211	total	244
concepts	declared	15	defined	23	total	38

Stage "B"

Ongoing. Context-sensitive subject equivalence for native type assignment.

Stage "A2": "Extending the Applicability Condition"

2015 October 9. λδ version 2A2 is started.

Stage "A1": "Extending the Applicability Condition"

2015 August 27. λδ version 2A1 appears too complex and is dismissed.

2014 October 28. λδ version 2A1 is released.

2014 September 9. Iterated static type assignment defined (more elegantly) as a primitive notion.

2014 June 18. Preservation of stratified native validity for context-sensitive computation on terms.

2014 June 9. Strong qrst-normalization for simply typed terms.

2014 April 16. Lazy equivalence on local environments added as q-step to rst-computation on closures (anniversary milestone).

2014 January 20. Parametrized slicing of local environments comprises both versions of this operation (one from basic_1, the other used in basic_2 till now).

2013 August 7. Passive support for global environments.

2013 July 27. Reaxiomatized β-reductum as in rt-reduction.

2013 July 20. Context-sensitive strong rt-normalization for simply typed terms.

2013 April 16. Reaxiomatized substitution and reduction commute with respect to subclosure (anniversary milestone).

2013 March 16. Mutual recursive preservation of stratified native validity for rst-computation on closures.

2012 October 16. Confluence for context-free parallel reduction on closures.

2012 July 26. Term binders polarized to control ζ-reduction (not released).

2012 April 16. Context-sensitive subject equivalence for atomic arity assignment (anniversary milestone).

2012 March 15. Context-sensitive strong normalization for simply typed terms.

2012 January 27. Support for abstract candidates of reducibility.

2011 September 21. Confluence for context-sensitive parallel reduction on terms.

2011 September 6. Confluence for context-free parallel reduction on terms.

2011 April 17. λδ version 2 is started.

Logical Structure of the Specification [spacer]

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

component	plane	files
relocation	ranged equivalence for closures	freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )	freq_freq
	context-sensitive free variables	frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )	frees_weight frees_lreq frees_frees
	generic slicing for local environments	drops_vector ( ⬇*[?,?] ? ≡ ? )
		drops ( ⬇*[?,?] ? ≡ ? )	drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
	generic relocation for terms	lifts_vector ( ⬆*[?] ? ≡ ? )	lifts_lift_vector
		lifts ( ⬆*[?] ? ≡ ? )	lifts_simple lifts_weight lifts_lifts
	ranged equivalence for local environments	lreq ( ? ≡[?] ? )	lreq_length lreq_lreq
	generic entrywise extension of context-sensitive relations for terma	lexs ( ? ⦻*[?,?,?] ? )	lexs_length lexs_lexs

grammar	context-sensitive equivalences for terms	ceq	ceq_ceq
	same top term structure	tsts ( ? ≂ ? )	tsts_tsts tsts_vector
	closures	cl_weight ( ♯{?,?,?} )	cl_restricted_weight ( ♯{?,?} )
	internal syntax	genv
		lenv	lenv_weight ( ♯{?} )	lenv_length ( \|?\| )	lenv_append ( ? @@ ? )
		term	term_weight ( ♯{?} )	term_simple ( 𝐒⦃?⦄ )	term_vector ( Ⓐ?.? )
		item
	external syntax	aarity

[Valid XHTML 1.1]

[Valid CSS level 2]

[Generated from XML via XSL]

[PNG used here]

[Viewable with any browser]

Last update: Sun, 27 Mar 2016 18:42:29 +0200