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 = "lambdadelta version 2"
   5       title = "lambdadelta 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="2013 August 7.">
  37          Passive support for global environments.
  38    </news>
  39    <news date="2013 July 27.">
  40          Reaxiomatized β-reductum as in extended β-reduction
  41    </news>
  42    <news date="2013 July 20.">
  43          Context-sensitive extended strong normalization
  44          for simply typed terms.
  45    </news>
  46    <news date="2013 April 16.">
  47          Reaxiomatized substitution and reduction
  48          commute with respect to subclosure
  49          (anniversary milestone).
  50    </news>
  51    <news date="2013 March 16.">
  52          Mutual recursive preservation of stratified native validity
  53          for hyper computation on closures.
  54    </news>
  55    <news date="2012 October 16.">
  56          Confluence for context-free parallel reduction on closures.
  57    </news>
  58    <news date="2012 July 26.">
  59          Term binders polarized to control ζ-reduction.
  60    </news>
  61    <news date="2012 April 16.">
  62          Context-sensitive subject equivalence
  63          for atomic arity assignment
  64          (anniversary milestone).
  65    </news>
  66    <news date="2012 March 15.">
  67          Context-sensitive strong normalization
  68          for simply typed terms.
  69    </news>
  70    <news date="2012 January 27.">
  71          Support for abstract candidates of reducibility.
  72    </news>
  73    <news date="2011 September 21.">
  74          Confluence for context-sensitive parallel reduction on terms.
  75    </news>
  76    <news date="2011 September 6.">
  77          Confluence for context-free parallel reduction on terms.
  78    </news>
  79    <news date="2011 April 17.">
  80          Specification starts.
  81    </news>
  82
  83    <section>Logical Structure of the Specification</section>
  84    <body>The source files are grouped in planes and components
  85          according to the following table.
  86          A notation file covering the whole specification is provided.
  87          The notation for the relations or functions introduced in each file
  88          is shown in parentheses (? are placeholders).
  89    </body>
  90    <table name="basic_2_src"/>
  91
  92    <section>Physical Structure of the Specification</section>
  93    <body>The source files are grouped in directories,
  94          one for each component.
  95    </body>
  96    <footer/>
  97 </page>