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