matita/matita/contribs/lambdadelta/basic_2A/web/basic_2A.ldw.xml

   1 <?xml version="1.0" encoding="UTF-8"?>
   2
   3 <page xmlns="http://lambdadelta.info/"
   4       description = "\lambda\delta home page"
   5       title = "\lambda\delta home page"
   6       logo = "crux"
   7       head = "cic:/matita/lambdadelta/basic_2A/ (core λδ version 2A)"
   8 >
   9    <sitemap name="sitemap"/>
  10
  11    <section4 name="summary">Summary of the Specification</section4>
  12    <body>Here is a numerical account of the specification's contents
  13          and its timeline.
  14    </body>
  15    <table name="basic_2A_sum"/>
  16
  17    <news class="delta" date="2020-02-27.">
  18          λδ-2A is repackaged without λδ-ground.
  19    </news>
  20    <news class="delta" date="2019-11-20.">
  21          λδ-2A is repackaged (was λδ-2A1).
  22    </news>
  23    <news class="delta" date="2015-08-27.">
  24          λδ-2A appears too complex and is dismissed.
  25    </news>
  26    <news class="gamma" date="2014-10-28.">
  27          λδ-2A is released.
  28    </news>
  29    <news class="beta" date="2014-09-09.">
  30          Iterated static type assignment defined (more elegantly)
  31          as a primitive notion.
  32    </news>
  33    <news class="beta" date="2014-06-18.">
  34          Preservation of stratified native validity
  35          for context-sensitive computation on terms.
  36    </news>
  37    <news class="alpha" date="2014-06-09.">
  38          Strong qrst-normalization
  39          for simply typed terms.
  40    </news>
  41    <news class="alpha" date="2014-04-16.">
  42          Lazy equivalence on local environments
  43          added as q-step to rst-computation on closures
  44          (anniversary milestone).
  45    </news>
  46    <news class="alpha" date="2014-01-20.">
  47          Parametrized slicing on local environments
  48          comprises both versions of this operation
  49          (one from basic_1, the other used in basic_2 till now).
  50    </news>
  51    <news class="alpha" date="2013-08-07.">
  52          Passive support for global environments.
  53    </news>
  54    <news class="alpha" date="2013-07-27.">
  55          Reaxiomatized β-reductum as in rt-reduction.
  56    </news>
  57    <news class="alpha" date="2013-07-20.">
  58          Context-sensitive strong rt-normalization
  59          for simply typed terms.
  60    </news>
  61    <news class="alpha" date="2013-04-16.">
  62          Reaxiomatized substitution and reduction
  63          commute with respect to subclosure
  64          (anniversary milestone).
  65    </news>
  66    <news class="alpha" date="2013-03-16.">
  67          Mutual recursive preservation of stratified native validity
  68          for rst-computation on closures.
  69    </news>
  70    <news class="alpha" date="2012-10-16.">
  71          Confluence for context-free parallel reduction on closures.
  72    </news>
  73    <news class="alpha" date="2012-07-26.">
  74          Term binders polarized to control ζ-reduction (not released).
  75    </news>
  76    <news class="alpha" date="2012-04-16.">
  77          Context-sensitive subject equivalence
  78          for atomic arity assignment
  79          (anniversary milestone).
  80    </news>
  81    <news class="alpha" date="2012-03-15.">
  82          Context-sensitive strong normalization
  83          for simply typed terms.
  84    </news>
  85    <news class="alpha" date="2012-01-27.">
  86          Generic candidates of reducibility.
  87    </news>
  88    <news class="alpha" date="2011-09-21.">
  89          Confluence for context-sensitive parallel reduction on terms.
  90    </news>
  91    <news class="alpha" date="2011-09-06.">
  92          Confluence for context-free parallel reduction on terms.
  93    </news>
  94    <news class="alpha" date="2011-04-17.">
  95          λδ-2A is started.
  96    </news>
  97 <!--
  98    <section4 name="structure">Logical Structure of the Specification</section4>
  99    <body>This table reports the specification's components and their planes.
 100    </body>
 101    <table name="basic_2A_src"/>
 102 -->
 103    <footer/>
 104 </page>