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