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    <news date="In progress.">
  31          Context-sensitive subject equivalence
  32          for native type assignment.
  33    </news>
  34    <news date="In progress.">
  35          Closure of native validity
  36          for context-sensitive extended computation.
  37    </news>
  38    <news date="2014 April 16.">
  39          lazy equivalence for local environments
  40          serves as irrelevant step in "big tree" computation
  41          (anniversary milestone).
  42    </news>
  43    <news date="2014 January 20.">
  44          Parametrized slicing for local environments
  45          comprises both versions of this operation
  46          (one from basic_1, the other used in basic_2 till now).
  47    </news>
  48    <news date="2013 August 7.">
  49          Passive support for global environments.
  50    </news>
  51    <news date="2013 July 27.">
  52          Reaxiomatized β-reductum as in extended β-reduction
  53    </news>
  54    <news date="2013 July 20.">
  55          Context-sensitive extended strong normalization
  56          for simply typed terms.
  57    </news>
  58    <news date="2013 April 16.">
  59          Reaxiomatized substitution and reduction
  60          commute with respect to subclosure
  61          (anniversary milestone).
  62    </news>
  63    <news date="2013 March 16.">
  64          Mutual recursive preservation of stratified native validity
  65          for "big tree" computation on closures.
  66    </news>
  67    <news date="2012 October 16.">
  68          Confluence for context-free parallel reduction on closures.
  69    </news>
  70    <news date="2012 July 26.">
  71          Term binders polarized to control ζ-reduction (not released).
  72    </news>
  73    <news date="2012 April 16.">
  74          Context-sensitive subject equivalence
  75          for atomic arity assignment
  76          (anniversary milestone).
  77    </news>
  78    <news date="2012 March 15.">
  79          Context-sensitive strong normalization
  80          for simply typed terms.
  81    </news>
  82    <news date="2012 January 27.">
  83          Support for abstract candidates of reducibility.
  84    </news>
  85    <news date="2011 September 21.">
  86          Confluence for context-sensitive parallel reduction on terms.
  87    </news>
  88    <news date="2011 September 6.">
  89          Confluence for context-free parallel reduction on terms.
  90    </news>
  91    <news date="2011 April 17.">
  92          Specification starts.
  93    </news>
  94
  95    <section>Logical Structure of the Specification</section>
  96    <body>The source files are grouped in planes and components
  97          according to the following table.
  98          Notation files covering the whole specification are provided.
  99          The notation for the relations or functions introduced in each file
 100          is shown in parentheses (? are placeholders).
 101    </body>
 102    <table name="basic_2_src"/>
 103
 104    <section>Physical Structure of the Specification</section>
 105    <body>The source files are grouped in directories,
 106          one for each component.
 107    </body>
 108    <footer/>
 109 </page>