--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "\lambda\delta home page"
+ title = "\lambda\delta home page"
+ logo = "crux"
+ head = "cic:/matita/lambdadelta/basic_2A/ (core λδ version 2A)"
+>
+ <sitemap name="sitemap"/>
+
+ <section4 name="summary">Summary of the Specification</section4>
+ <body>Here is a numerical account of the specification's contents
+ and its timeline.
+ </body>
+ <table name="basic_2A_sum"/>
+
+ <news class="delta" date="2020-02-27.">
+ λδ-2A is repackaged on the basis of λδ-ground-2.
+ </news>
+ <news class="delta" date="2019-11-20.">
+ λδ-2A is repackaged (was λδ-2A1).
+ </news>
+ <news class="delta" date="2015-08-27.">
+ λδ-2A appears too complex and is dismissed.
+ </news>
+ <news class="gamma" date="2014-10-28.">
+ λδ-2A is released.
+ </news>
+ <news class="beta" date="2014-09-09.">
+ Iterated static type assignment defined (more elegantly)
+ as a primitive notion.
+ </news>
+ <news class="beta" date="2014-06-18.">
+ Preservation of stratified native validity
+ for context-sensitive computation on terms.
+ </news>
+ <news class="alpha" date="2014-06-09.">
+ Strong qrst-normalization
+ for simply typed terms.
+ </news>
+ <news class="alpha" date="2014-04-16.">
+ Lazy equivalence on local environments
+ added as q-step to rst-computation on closures
+ (anniversary milestone).
+ </news>
+ <news class="alpha" date="2014-01-20.">
+ Parametrized slicing on local environments
+ comprises both versions of this operation
+ (one from basic_1, the other used in basic_2 till now).
+ </news>
+ <news class="alpha" date="2013-08-07.">
+ Passive support for global environments.
+ </news>
+ <news class="alpha" date="2013-07-27.">
+ Reaxiomatized β-reductum as in rt-reduction.
+ </news>
+ <news class="alpha" date="2013-07-20.">
+ Context-sensitive strong rt-normalization
+ for simply typed terms.
+ </news>
+ <news class="alpha" date="2013-04-16.">
+ Reaxiomatized substitution and reduction
+ commute with respect to subclosure
+ (anniversary milestone).
+ </news>
+ <news class="alpha" date="2013-03-16.">
+ Mutual recursive preservation of stratified native validity
+ for rst-computation on closures.
+ </news>
+ <news class="alpha" date="2012-10-16.">
+ Confluence for context-free parallel reduction on closures.
+ </news>
+ <news class="alpha" date="2012-07-26.">
+ Term binders polarized to control ζ-reduction (not released).
+ </news>
+ <news class="alpha" date="2012-04-16.">
+ Context-sensitive subject equivalence
+ for atomic arity assignment
+ (anniversary milestone).
+ </news>
+ <news class="alpha" date="2012-03-15.">
+ Context-sensitive strong normalization
+ for simply typed terms.
+ </news>
+ <news class="alpha" date="2012-01-27.">
+ Generic candidates of reducibility.
+ </news>
+ <news class="alpha" date="2011-09-21.">
+ Confluence for context-sensitive parallel reduction on terms.
+ </news>
+ <news class="alpha" date="2011-09-06.">
+ Confluence for context-free parallel reduction on terms.
+ </news>
+ <news class="alpha" date="2011-04-17.">
+ λδ-2A is started.
+ </news>
+<!--
+ <section4 name="structure">Logical Structure of the Specification</section4>
+ <body>This table reports the specification's components and their planes.
+ </body>
+ <table name="basic_2A_src"/>
+-->
+ <footer/>
+</page>
projects / helm.git / blobdiff