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

   1 <?xml version="1.0" encoding="UTF-8"?>
   2
   3 <page xmlns="http://lambdadelta.info/"
   4       description = "\lambda\delta version 2"
   5       title = "\lambda\delta version 2"
   6       head = "cic:/matita/lambdadelta/basic_2/ (λδ version 2)"
   7 >
   8 <!--
   9    <section>System's Syntax and Behavior</section>
  10    <body>This is a summary of the "block structure"
  11          of the System's syntactic items and reductions.
  12    </body>
  13    <table name="basic_2_blk"/>
  14    <body>* In terms only.
  15          ** In terms and local environments only.
  16          *** In global environments only.
  17          **** Sort level k in terms only.
  18    </body>
  19 -->
  20
  21    <section>Summary of the Specification</section>
  22    <body>Here is a numerical acount of the specification's contents
  23          and its timeline.
  24          Nodes are counted according to the "intrinsinc complexity measure"
  25          [F. Guidi: "Procedural Representation of CIC Proof Terms"
  26          Journal of Automated Reasoning 44(1-2), Springer (February 2010),
  27          pp. 53-78].
  28    </body>
  29    <table name="basic_2_sum"/>
  30
  31    <subsection>Stage "B"</subsection>
  32    <news date="In progress.">
  33          Context-sensitive subject equivalence
  34          for native type assignment.
  35    </news>
  36
  37    <subsection>Stage "A": "Weakening the Applicability Condition"</subsection>
  38    <news date="2014 June 18.">
  39          Preservation of stratified native validity
  40          for context-sensitive computation on terms.
  41    </news>
  42    <news date="2014 June 9.">
  43          "Big tree" strong normalization
  44          for simply typed terms.
  45    </news>
  46    <news date="2014 April 16.">
  47          lazy equivalence on local environments
  48          serves as irrelevant step in "big tree" computation on closures
  49          (anniversary milestone).
  50    </news>
  51    <news date="2014 January 20.">
  52          Parametrized slicing for local environments
  53          comprises both versions of this operation
  54          (one from basic_1, the other used in basic_2 till now).
  55    </news>
  56    <news date="2013 August 7.">
  57          Passive support for global environments.
  58    </news>
  59    <news date="2013 July 27.">
  60          Reaxiomatized β-reductum as in extended β-reduction
  61    </news>
  62    <news date="2013 July 20.">
  63          Context-sensitive extended strong normalization
  64          for simply typed terms.
  65    </news>
  66    <news date="2013 April 16.">
  67          Reaxiomatized substitution and reduction
  68          commute with respect to subclosure
  69          (anniversary milestone).
  70    </news>
  71    <news date="2013 March 16.">
  72          Mutual recursive preservation of stratified native validity
  73          for "big tree" computation on closures.
  74    </news>
  75    <news date="2012 October 16.">
  76          Confluence for context-free parallel reduction on closures.
  77    </news>
  78    <news date="2012 July 26.">
  79          Term binders polarized to control ζ-reduction (not released).
  80    </news>
  81    <news date="2012 April 16.">
  82          Context-sensitive subject equivalence
  83          for atomic arity assignment
  84          (anniversary milestone).
  85    </news>
  86    <news date="2012 March 15.">
  87          Context-sensitive strong normalization
  88          for simply typed terms.
  89    </news>
  90    <news date="2012 January 27.">
  91          Support for abstract candidates of reducibility.
  92    </news>
  93    <news date="2011 September 21.">
  94          Confluence for context-sensitive parallel reduction on terms.
  95    </news>
  96    <news date="2011 September 6.">
  97          Confluence for context-free parallel reduction on terms.
  98    </news>
  99    <news date="2011 April 17.">
 100          Specification starts.
 101    </news>
 102
 103    <section>Logical Structure of the Specification</section>
 104    <body>The source files are grouped in planes and components
 105          according to the following table.
 106          Notation files covering the whole specification are provided.
 107          The notation for the relations or functions introduced in each file
 108          is shown in parentheses (? are placeholders).
 109    </body>
 110    <table name="basic_2_src"/>
 111
 112    <section>Physical Structure of the Specification</section>
 113    <body>The source files are grouped in directories,
 114          one for each component.
 115    </body>
 116    <footer/>
 117 </page>